Re: [isabelle] question



On 24/01/2014 17:54, John Wickerson wrote:
> Hi all,
> 
> I wonder if I might invite comment on the following statement?
> 
> "Don't even *think* about firing up Isabelle until you've completed a really solid pencil-and-paper proof of the theorem you want to mechanise."

That's easy to refute: Quickcheck and Nitpick may already give you feedback
during development. But your statement becomes monotonically truer with the
complexity of the theory.

Tobias




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