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/Decision_Procs/cooper_tac.ML
changeset 64244 e7102c40783c
parent 64243 aee949f6642d
child 64593 50c715579715 
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
@@ -50,7 +50,7 @@
           div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
           mod_self
           div_by_0 mod_by_0 div_0 mod_0
-          div_by_1 mod_by_1 div_1 mod_1
+          div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
           Suc_eq_plus1}
       addsimps @{thms ac_simps}
       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
isabelle