src/HOL/Real/RealDef.thy
changeset 27682 25aceefd4786
parent 27668 6eb20b2cecf8
child 27833 29151fa7c58e
     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -346,14 +346,12 @@
     1.4  apply (blast intro: real_trans_lemma)
     1.5  done
     1.6  
     1.7 -(* Axiom 'order_less_le' of class 'order': *)
     1.8 -lemma real_less_le: "((w::real) < z) = (w \<le> z & w \<noteq> z)"
     1.9 -by (simp add: real_less_def)
    1.10 -
    1.11  instance real :: order
    1.12 -proof qed
    1.13 - (assumption |
    1.14 -  rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+
    1.15 +proof
    1.16 +  fix u v :: real
    1.17 +  show "u < v \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> u" 
    1.18 +    by (auto simp add: real_less_def intro: real_le_anti_sym)
    1.19 +qed (assumption | rule real_le_refl real_le_trans real_le_anti_sym)+
    1.20  
    1.21  (* Axiom 'linorder_linear' of class 'linorder': *)
    1.22  lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
    1.23 @@ -361,7 +359,6 @@
    1.24  apply (auto simp add: real_le real_zero_def add_ac)
    1.25  done
    1.26  
    1.27 -
    1.28  instance real :: linorder
    1.29    by (intro_classes, rule real_le_linear)
    1.30