# HG changeset patch
# User kleing
# Date 1081835312 -7200
# Node ID b13da5649bf92796ab938f3f2eb332dd9c36f35f
# Parent  ea6e18e5c7a97d4fd07a5fc9d060ede73f9ed2b2
hence -> from calculation have

diff -r ea6e18e5c7a9 -r b13da5649bf9 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Tue Apr 13 07:47:31 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Tue Apr 13 07:48:32 2004 +0200
@@ -388,15 +388,16 @@
     show "x * y \<notin> mult_set A B"
     proof -
       { fix u::rat and v::rat
-	assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
-	moreover
-	with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
-	moreover
-	with prems have "0\<le>v"
-	  by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
-	moreover
-	hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
-	ultimately have False by force}
+	      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
+	      moreover
+	      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
+	      moreover
+	      with prems have "0\<le>v"
+	        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
+	      moreover
+        from calculation
+	      have "u*v < x*y" by (blast intro: mult_strict_mono prems)
+	      ultimately have False by force }
       thus ?thesis by (auto simp add: mult_set_def)
     qed
   qed