tuned;

--- a/src/HOL/Hyperreal/ex/Sqrt.thy	Wed Mar 06 17:56:02 2002 +0100
+++ b/src/HOL/Hyperreal/ex/Sqrt.thy	Wed Mar 06 18:16:48 2002 +0100
@@ -23,7 +23,8 @@
   \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
 proof -
   assume "x \<in> \<rat>"
-  then obtain m n :: nat where n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
+  then obtain m n :: nat where
+      n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
     by (unfold rationals_def) blast
   let ?gcd = "gcd (m, n)"
   from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
@@ -40,7 +41,8 @@
   moreover
   have "\<bar>x\<bar> = real ?k / real ?l"
   proof -
-    from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)"
+    from gcd have "real ?k / real ?l =
+        real (?gcd * ?k) / real (?gcd * ?l)"
       by (simp add: real_mult_div_cancel1)
     also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
     also from x_rat have "\<dots> = \<bar>x\<bar>" ..
@@ -103,12 +105,6 @@
   with p show False by simp
 qed
 
-text {*
-  Just for the record: we instantiate the main theorem for the
-  specific prime number @{text 2} (real mathematicians would never do
-  this formally :-).
-*}
-
 corollary "sqrt (real (2::nat)) \<notin> \<rat>"
   by (rule sqrt_prime_irrational) (rule two_is_prime)
 

--- a/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 17:56:02 2002 +0100
+++ b/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 18:16:48 2002 +0100
@@ -23,8 +23,8 @@
   apply (rule_tac j = "k * k" in dvd_mult_left, simp)
   done
 
-lemma reduction:
-    "p \<in> prime \<Longrightarrow> 0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
+lemma reduction: "p \<in> prime \<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)
   apply (erule disjE)