Re: [isabelle] question
I can say that I "hate" firing up Isabelle before having made at least a
proof sketch of the statement
I want to prove. I don´t feel comfortable with automation unless I know
what is going on.
On Fri, Jan 24, 2014 at 2:54 PM, John Wickerson <johnwickerson at cantab.net>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."
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and