src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Orderings.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -39,9 +39,6 @@
 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
 unfolding less_le by blast
 
-lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
-by (erule contrapos_pn, erule subst, rule less_irrefl)
-
 
 text {* Useful for simplification, but too risky to include by default. *}