--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 23:46:03 2009 +0100
@@ -99,7 +99,7 @@
addsimps [refl,nat_mod_add_eq,
@{thm "mod_self"}, @{thm "zmod_self"},
@{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_plus1"}]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]