update examples for Isabelle2005;

3 files changed, 21 insertions, 17 deletions

diff --git a/isar/Example-Xsym.thy b/isar/Example-Xsym.thy
index 50376096..d9b6a415 100644
--- a/isar/Example-Xsym.thy
+++ b/isar/Example-Xsym.thy
@@ -4,7 +4,7 @@
       $Id$
 *)
 
-theory Example imports Main begin
+theory "Example-Xsym" imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
 
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
diff --git a/isar/Root2_Tactic.thy b/isar/Root2_Tactic.thy
index 35646ada..7c0620c5 100644
--- a/isar/Root2_Tactic.thy
+++ b/isar/Root2_Tactic.thy
@@ -1,16 +1,18 @@
 (* Example proof by Larry Paulson; see http://www.cs.kun.nl/~freek/comparison/ 
-   Taken from Isabelle2004 distribution. *)
+   Taken from Isabelle2005 distribution. *)
 
 
 (*  Title:      HOL/Hyperreal/ex/Sqrt_Script.thy
-    ID:         Id: Sqrt_Script.thy,v 1.3 2003/12/10 14:59:35 paulson Exp 
+    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 *)
 
 header {* Square roots of primes are irrational (script version) *}
 
-theory Sqrt_Script imports Primes Complex_Main begin
+theory Root2_Tactic
+imports Primes Complex_Main
+begin
 
 text {*
   \medskip Contrast this linear Isabelle/Isar script with Markus
@@ -19,16 +21,16 @@ text {*
 
 subsection {* Preliminaries *}
 
-lemma prime_nonzero:  "p \<in> prime \<Longrightarrow> p \<noteq> 0"
+lemma prime_nonzero:  "prime p \<Longrightarrow> p \<noteq> 0"
   by (force simp add: prime_def)
 
 lemma prime_dvd_other_side:
-    "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
+    "n * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
   apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
   apply (rule_tac j = "k * k" in dvd_mult_left, simp)
   done
 
-lemma reduction: "p \<in> prime \<Longrightarrow>
+lemma reduction: "prime p \<Longrightarrow>
     0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
   apply (rule ccontr)
   apply (simp add: linorder_not_less)
@@ -42,7 +44,7 @@ lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j *
   by (simp add: mult_ac)
 
 lemma prime_not_square:
-    "p \<in> prime \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
+    "prime p \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
   apply (induct m rule: nat_less_induct)
   apply clarify
   apply (frule prime_dvd_other_side, assumption)
@@ -67,7 +69,7 @@ text {*
 *}
 
 theorem prime_sqrt_irrational:
-    "p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
+    "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
   apply (simp add: rationals_def real_abs_def)
   apply clarify
   apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)