Re: [isabelle] proof statement fails



On 07.07.2012 13:43, John Wickerson wrote:
So maybe the following will work...

lemma "(2 :: nat) + 2 = 4"
   proof(auto)

It would; but as a rule of thumb, auto should never be the argument of proof command: The result of auto is very much unpredictable and unstable across versions, so chances that your proof will break some not so far time in the future are pretty high.

  -- Lars





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