src/HOL/Decision_Procs/mir_tac.ML
changeset 30031 bd786c37af84
parent 29948 cdf12a1cb963
child 30034 60f64f112174
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Feb 20 21:29:34 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Feb 20 23:46:03 2009 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4                          addsimps [refl,nat_mod_add_eq, 
     1.5                                    @{thm "mod_self"}, @{thm "zmod_self"},
     1.6                                    @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
     1.7 -                                  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.8 +                                  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.9                                    @{thm "Suc_plus1"}]
    1.10                          addsimps @{thms add_ac}
    1.11                          addsimprocs [cancel_div_mod_proc]