Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deleted the obsolete nat_neqE
authorpaulson
Wed, 10 Jan 2001 11:15:24 +0100
changeset 10851 31ac62e3a0ed
parent 10850 e1a793957a8f
child 10852 49868b703e4d
deleted the obsolete nat_neqE
src/HOL/Lambda/Lambda.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle