# HG changeset patch
# User wenzelm
# Date 1005086855 -3600
# Node ID d46a32262bac7a58e58a137ef565c7ee23c3e984
# Parent  8f41684d90e68382e165ddccda67b4de9ea92981
activate dead code, make document work;

diff -r 8f41684d90e6 -r d46a32262bac src/HOL/Real/ex/ROOT.ML
--- a/src/HOL/Real/ex/ROOT.ML	Tue Nov 06 23:47:03 2001 +0100
+++ b/src/HOL/Real/ex/ROOT.ML	Tue Nov 06 23:47:35 2001 +0100
@@ -5,5 +5,6 @@
 *)
 
 no_document use_thy "Primes";
-time_use_thy "Sqrt_Irrational";
+time_use_thy "Sqrt";
+time_use_thy "Sqrt_Script";
 time_use_thy "BinEx";
diff -r 8f41684d90e6 -r d46a32262bac src/HOL/Real/ex/Sqrt_Script.thy
--- a/src/HOL/Real/ex/Sqrt_Script.thy	Tue Nov 06 23:47:03 2001 +0100
+++ b/src/HOL/Real/ex/Sqrt_Script.thy	Tue Nov 06 23:47:35 2001 +0100
@@ -6,13 +6,13 @@
 
 header {*  Square roots of primes are irrational *}
 
+theory Sqrt_Script = Primes + Real:
+
 text {*
-  \medskip Contrast this linear Isar script with Markus Wenzel's 
-           more mathematical version.
+  \medskip Contrast this linear Isar script with Markus Wenzel's more
+  mathematical version.
 *}
 
-theory Sqrt_Script = Primes + Real:
-
 section {* Preliminaries *}
 
 lemma prime_nonzero:  "p \<in> prime \<Longrightarrow> p\<noteq>0"
@@ -56,8 +56,8 @@
 section {* Main theorem *}
 
 text {*
-  \tweakskip The square root of any prime number (including @{text 2})
-  is irrational.
+  The square root of any prime number (including @{text 2}) is
+  irrational.
 *}
 
 theorem prime_sqrt_irrational: "\<lbrakk>p \<in> prime; x*x = real p; 0 \<le> x\<rbrakk> \<Longrightarrow> x \<notin> \<rat>"
@@ -66,12 +66,12 @@
 apply (erule_tac P="real m / real n * ?x = ?y" in rev_mp) 
 apply (simp del: real_of_nat_mult
 	    add: real_divide_eq_eq prime_not_square
-                 real_of_nat_mult [THEN sym])
+                 real_of_nat_mult [symmetric])
 done
 
 lemma two_is_prime: "2 \<in> prime"
 apply (auto simp add: prime_def)
-apply (case_tac "m")
+apply (case_tac m)
 apply (auto dest!: dvd_imp_le)
 apply arith
 done