diff options
| author | Makarius Wenzel | 2005-09-17 11:10:30 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2005-09-17 11:10:30 +0000 |
| commit | 5306636f1baafb513df058260493f7a80fddfc43 (patch) | |
| tree | 5645f7063ca5f66de47227c01539d1ff359aa6d0 /isar/Root2_Isar.thy | |
| parent | 8745d32b0be33418e9ada81001802185f00e7f90 (diff) | |
update examples for Isabelle2005;
Diffstat (limited to 'isar/Root2_Isar.thy')
| -rw-r--r-- | isar/Root2_Isar.thy | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/isar/Root2_Isar.thy b/isar/Root2_Isar.thy index e02ef5fb..7a0123dd 100644 --- a/isar/Root2_Isar.thy +++ b/isar/Root2_Isar.thy @@ -1,16 +1,18 @@ (* Example proof by Markus Wenzel; see http://www.cs.kun.nl/~freek/comparison/ - Taken from Isabelle2004 distribution. *) + Taken from Isabelle2005 distribution. *) (* Title: HOL/Hyperreal/ex/Sqrt.thy - ID: Id: Sqrt.thy,v 1.4 2004/01/12 15:51:47 paulson Exp + ID: $Id$ Author: Markus Wenzel, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) + *) header {* Square roots of primes are irrational *} -theory Root2_Isar imports Primes Complex_Main begin +theory Root2_Isar +imports Primes Complex_Main +begin subsection {* Preliminaries *} @@ -76,9 +78,9 @@ text {* irrational. *} -theorem sqrt_prime_irrational: "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>" +theorem sqrt_prime_irrational: "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>" proof - assume p_prime: "p \<in> prime" + assume p_prime: "prime p" then have p: "1 < p" by (simp add: prime_def) assume "sqrt (real p) \<in> \<rat>" then obtain m n where @@ -121,9 +123,9 @@ text {* structure, it is probably closer to proofs seen in mathematics. *} -theorem "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>" +theorem "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>" proof - assume p_prime: "p \<in> prime" + assume p_prime: "prime p" then have p: "1 < p" by (simp add: prime_def) assume "sqrt (real p) \<in> \<rat>" then obtain m n where |