Re: [isabelle] question
I am an old time Isabelle user, and someone with a PhD in math
(abstract algebra), and I always do my work in Isabelle straight out.
It's my scratch pad. I make lots of lemmas and start with a heavy use
of sorry, but the use of Isabelle as a record keeper when you are
thrashing out a proof is considerable. It is true that you will
probably make a very messy proof at best if you try to use Isabelle to
bludgeoned the proof to death or just start failing with the
connectives. Also, I basically never use auto, and only use clarsimp
when I know what I want it to do and what it will do. But through the
use of lemmas and subgoals, you can use Isabelle to help you
interactively discover the proof of theorems you are trying to prove.
On 1/24/14 10:54 AM, John Wickerson wrote:
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."
This archive was generated by a fusion of
Pipermail (Mailman edition) and