[isabelle] a simplifier question



hi.

can someone explain to me why the first proof succeeds, while the second
fails?
I looked into the simplifier trace info but didn't understand too much.

thanx




theory tmp
imports Main Real NthRoot Transcendental
begin

    lemma
        fixes   a b c::real
        assumes "a>0" "b>0" "c>0"
        shows   "a+b+c > 0"
    using [[simp_trace=true]]
    using assms
    apply (simp)
    done


    lemma
        fixes   a b c::real
        assumes "a>0" "b>0" "c>0"
        shows   "a+b+c > 0"
    using [[simp_trace=true]]
    apply (simp add:assms)
    done

end


-- 
I can't see very far,
I must be standing on the shoulders of midgets.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.