1.1 --- a/src/HOL/Real/PReal.thy	Tue Apr 13 07:47:31 2004 +0200
     1.2 +++ b/src/HOL/Real/PReal.thy	Tue Apr 13 07:48:32 2004 +0200
     1.3 @@ -388,15 +388,16 @@
     1.4      show "x * y \<notin> mult_set A B"
     1.5      proof -
     1.6        { fix u::rat and v::rat
     1.7 -	assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
     1.8 -	moreover
     1.9 -	with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
    1.10 -	moreover
    1.11 -	with prems have "0\<le>v"
    1.12 -	  by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
    1.13 -	moreover
    1.14 -	hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
    1.15 -	ultimately have False by force}
    1.16 +	      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
    1.17 +	      moreover
    1.18 +	      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
    1.19 +	      moreover
    1.20 +	      with prems have "0\<le>v"
    1.21 +	        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
    1.22 +	      moreover
    1.23 +        from calculation
    1.24 +	      have "u*v < x*y" by (blast intro: mult_strict_mono prems)
    1.25 +	      ultimately have False by force }
    1.26        thus ?thesis by (auto simp add: mult_set_def)
    1.27      qed
    1.28    qed