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}]