src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Nat.thy	Wed May 04 08:36:10 2005 +0200
@@ -443,6 +443,8 @@
     (assumption |
       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
 
+lemmas linorder_neqE_nat = linorder_neqE[where 'a = nat]
+
 lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   by (blast elim!: less_SucE)