src/HOL/Decision_Procs/mir_tac.ML

              @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"},
              @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"},
              @{thm "divide_zero"}, 
              @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
              @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
-             @{thm "diff_minus"}, @{thm "minus_divide_left"}]
+             @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
 val comp_ths = ths @ comp_arith @ @{thms simp_thms};
 
 
 val zdvd_int = @{thm "zdvd_int"};
 val zdiff_int_split = @{thm "zdiff_int_split"};