src/HOL/Orderings.thy
changeset 26300 03def556e26e
parent 26014 00c2c3525bef
child 26324 456f726a11e4
     1.1 --- a/src/HOL/Orderings.thy	Mon Mar 17 18:36:04 2008 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Mar 17 18:37:00 2008 +0100
     1.3 @@ -39,9 +39,6 @@
     1.4  lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
     1.5  unfolding less_le by blast
     1.6  
     1.7 -lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
     1.8 -by (erule contrapos_pn, erule subst, rule less_irrefl)
     1.9 -
    1.10  
    1.11  text {* Useful for simplification, but too risky to include by default. *}
    1.12