Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Integ/int_arith1.ML
changeset 12018 ec054019c910
parent 11868 56db9f3a6b3e
child 12482 d2848ccc9757 
--- a/src/HOL/Integ/int_arith1.ML	Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Fri Nov 02 17:55:24 2001 +0100
@@ -407,7 +407,7 @@
 val add_rules = 
     simp_thms @ bin_arith_simps @ bin_rel_simps @ 
     [int_numeral_0_eq_0, int_numeral_1_eq_1,
-     zadd_0, zadd_0_right, zdiff_def,
+     zminus_0, zadd_0, zadd_0_right, zdiff_def,
      zadd_zminus_inverse, zadd_zminus_inverse2, 
      zmult_0, zmult_0_right, 
      zmult_1, zmult_1_right,
isabelle