# HG changeset patch
# User haftmann
# Date 1265634403 -3600
# Node ID e47934673b74138cfc2508b4d4a9d2844fe65d29
# Parent  7efe662e41b46b51477ffa5352c872664be24bb2
tuned proof

diff -r 7efe662e41b4 -r e47934673b74 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 14:06:41 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 14:06:43 2010 +0100
@@ -2187,10 +2187,7 @@
   {assume dc: "?c*?d < 0" 
 
     from dc one_plus_one_pos[where ?'a='a] have dc': "(1 + 1)*?c *?d < 0"
-      apply (simp add: mult_less_0_iff field_simps) 
-      apply (rule add_neg_neg)
-      apply (simp_all add: mult_less_0_iff)
-      done
+      by (simp add: mult_less_0_iff field_simps) 
     hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
     have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"