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.
got rid of superfluous linorder_neqE-instance for int.
authornipkow
Wed, 15 Feb 2006 19:01:09 +0100
changeset 19044 d4bc0ee9383a
parent 19043 6c0fca729f33
child 19045 75786c2eb897
got rid of superfluous linorder_neqE-instance for int.
src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions
src/HOL/Integ/int_arith1.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/IntDef.thy	Wed Feb 15 18:10:09 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Wed Feb 15 19:01:09 2006 +0100
@@ -281,7 +281,6 @@
 
 
 lemmas zless_linear = linorder_less_linear [where 'a = int]
-lemmas linorder_neqE_int = linorder_neqE[where 'a = int]
 
 
 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
--- a/src/HOL/Integ/int_arith1.ML	Wed Feb 15 18:10:09 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Wed Feb 15 19:01:09 2006 +0100
@@ -526,7 +526,7 @@
     mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
     inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
     lessD = lessD @ [zless_imp_add1_zle],
-    neqE = thm "linorder_neqE_int" :: neqE,
+    neqE = neqE,
     simpset = simpset addsimps add_rules
                       addsimprocs simprocs
                       addcongs [if_weak_cong]}) #>
isabelle