--- 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)