diff -r d7bb6e4f5f82 -r d3be9be2b307 src/HOL/Hyperreal/ex/Sqrt_Script.thy
--- 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)