diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Feb 19 10:41:32 2004 +0100
+++ b/src/HOL/Set.thy	Thu Feb 19 15:57:34 2004 +0100
@@ -1963,15 +1963,6 @@
 lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
   by (rule subsetD)
 
-lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
-  by (simp add: order_less_le)
-
-lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
-  by (simp add: order_less_le)
-
-lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
-  by (rule order_less_asym)
-
 lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
   by (rule subst)