src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 67091 1393c2340eec
parent 63523 54e932f0c30a
child 67271 48ef58c6cf4c
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -1018,8 +1018,8 @@
     1.4            addsimps [@{thm power_divide}]
     1.5          val th =
     1.6            Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
     1.7 -            (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
     1.8 -             else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
     1.9 +            (if ord then @{lemma "(d=0 \<longrightarrow> P) \<and> (d>0 \<longrightarrow> P) \<and> (d<(0::real) \<longrightarrow> P) \<Longrightarrow> P" by auto}
    1.10 +             else @{lemma "(d=0 \<longrightarrow> P) \<and> (d \<noteq> (0::real) \<longrightarrow> P) \<Longrightarrow> P" by blast})
    1.11        in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
    1.12  
    1.13  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);