# [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.*