*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] question*From*: Joachim Breitner <breitner at kit.edu>*Date*: Fri, 24 Jan 2014 17:12:13 +0000*In-reply-to*: <866E7D87-1D8F-459E-808D-3DDE9D30EA11@cantab.net>*References*: <866E7D87-1D8F-459E-808D-3DDE9D30EA11@cantab.net>

Hi, Am Freitag, den 24.01.2014, 16:54 +0000 schrieb John Wickerson: > 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." it is certainly good advice, but Isabelle has its merits also when exploring and finding a proof. One could also say „Don’t even *think* about completing as solid pencil-and-paper proof of your theorem until you have finalized your formalisation, your definition, and your theorem.“ Because when you change some of these, fixing a pencil-and-paper-proof is tedious and error-prone, while Isabelle will easily tell you where you need to adjust stuff. So while there were certainly cases where I should have worked on paper before, I would not make it an absolute rule. Also, depending on your hand writing, there are good reason to avoid pen-and-pencil proofs that need to be readable even the next day :-) Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**References**:**[isabelle] question***From:*John Wickerson

- Previous by Date: Re: [isabelle] question
- Next by Date: Re: [isabelle] question
- Previous by Thread: [isabelle] Fwd: question
- Next by Thread: Re: [isabelle] question
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list