src/HOL/Set.thy
changeset 14398 c5c47703f763
parent 14381 1189a8212a12
child 14479 0eca4aabf371
     1.1 --- a/src/HOL/Set.thy	Thu Feb 19 10:41:32 2004 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Feb 19 15:57:34 2004 +0100
     1.3 @@ -1963,15 +1963,6 @@
     1.4  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
     1.5    by (rule subsetD)
     1.6  
     1.7 -lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
     1.8 -  by (simp add: order_less_le)
     1.9 -
    1.10 -lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
    1.11 -  by (simp add: order_less_le)
    1.12 -
    1.13 -lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
    1.14 -  by (rule order_less_asym)
    1.15 -
    1.16  lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
    1.17    by (rule subst)
    1.18