--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Apr 04 17:58:25 2014 +0100
@@ -1167,7 +1167,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -1184,7 +1184,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -1201,7 +1201,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1217,7 +1217,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1233,7 +1233,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1249,7 +1249,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }