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.

Best!


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



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
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.