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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and