# HG changeset patch
# User paulson
# Date 979121724 -3600
# Node ID 31ac62e3a0ed6710419a65bb5593aa952292044b
# Parent  e1a793957a8f43326a09f33293fc6762667bbf66
deleted the obsolete nat_neqE

diff -r e1a793957a8f -r 31ac62e3a0ed src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Jan 10 11:14:30 2001 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Wed Jan 10 11:15:24 2001 +0100
@@ -150,7 +150,7 @@
     apply (simp_all
       add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
       split: nat.split)
-  apply (auto elim: nat_neqE)
+  apply (auto simp add: linorder_neq_iff)
   done