src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 35033 e47934673b74
parent 35028 108662d50512
child 35045 a77d200e6503
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 14:06:41 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 14:06:43 2010 +0100
     1.3 @@ -2187,10 +2187,7 @@
     1.4    {assume dc: "?c*?d < 0" 
     1.5  
     1.6      from dc one_plus_one_pos[where ?'a='a] have dc': "(1 + 1)*?c *?d < 0"
     1.7 -      apply (simp add: mult_less_0_iff field_simps) 
     1.8 -      apply (rule add_neg_neg)
     1.9 -      apply (simp_all add: mult_less_0_iff)
    1.10 -      done
    1.11 +      by (simp add: mult_less_0_iff field_simps) 
    1.12      hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
    1.13      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
    1.14      have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"