--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 01:12:40 2013 +0200
@@ -2168,7 +2168,6 @@
by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
moreover
- moreover
{assume c: "?c = 0" and d: "?d>0"
from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
from d have d': "2*?d \<noteq> 0" by simp
@@ -2314,7 +2313,6 @@
by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
moreover
- moreover
{assume c: "?c = 0" and d: "?d>0"
from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
from d have d': "2*?d \<noteq> 0" by simp