--- a/src/HOL/Decision_Procs/Cooper.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Jul 19 16:09:44 2010 +0200
@@ -1356,7 +1356,7 @@
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
- apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
+ apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
@@ -1368,7 +1368,7 @@
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
- apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
+ apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]