Re: [isabelle] question

Hi John,

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>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."
> Thanks!
> John

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 MHonArc.