--- a/src/HOL/Tools/numeral_simprocs.ML Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Jul 19 16:09:44 2010 +0200
@@ -734,7 +734,7 @@
@{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_times_eq"},
@{thm "divide_divide_eq_right"},
- @{thm "diff_def"}, @{thm "minus_divide_left"},
+ @{thm "diff_minus"}, @{thm "minus_divide_left"},
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
@{thm field_divide_inverse} RS sym, @{thm inverse_divide},
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))