src/HOL/Real/RealDef.thy
changeset 15542 ee6cd48cf840
parent 15229 1eb23f805c06
child 15923 01d5d0c1c078
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon Feb 21 18:04:28 2005 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Mon Feb 21 19:23:46 2005 +0100
     1.3 @@ -353,7 +353,7 @@
     1.4  done
     1.5  
     1.6  lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
     1.7 -by (cases z, cases w, simp add: real_le order_antisym)
     1.8 +by (cases z, cases w, simp add: real_le)
     1.9  
    1.10  lemma real_trans_lemma:
    1.11    assumes "x + v \<le> u + y"
    1.12 @@ -368,7 +368,7 @@
    1.13      by (simp add: preal_add_le_cancel_left prems) 
    1.14    also have "... = (u'+y) + (u+v)"  by (simp add: preal_add_ac)
    1.15    finally show ?thesis by (simp add: preal_add_le_cancel_right)
    1.16 -qed						 
    1.17 +qed
    1.18  
    1.19  lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
    1.20  apply (cases i, cases j, cases k)
    1.21 @@ -401,7 +401,7 @@
    1.22  apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
    1.23                        preal_add_ac)
    1.24  apply (simp_all add: preal_add_assoc [symmetric] preal_cancels)
    1.25 -done 
    1.26 +done
    1.27  
    1.28  lemma real_add_left_mono: 
    1.29    assumes le: "x \<le> y" shows "z + x \<le> z + (y::real)"