author kleing Tue, 13 Apr 2004 07:48:32 +0200 changeset 14550 b13da5649bf9 parent 14549 ea6e18e5c7a9 child 14551 2cb6ff394bfb
hence -> from calculation have
 src/HOL/Real/PReal.thy file | annotate | diff | comparison | revisions
```--- 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```