*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Length of Proofs*From*: Makarius <makarius at sketis.net>*Date*: Tue, 20 Nov 2012 12:33:38 +0100 (CET)*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, Jens Doll <jd at cococo.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50AABBDD.70700@rsise.anu.edu.au>*References*: <50921697.9090307@cococo.de> <50921DCB.6050502@rsise.anu.edu.au> <alpine.LNX.2.00.1211162218270.24652@macbroy20.informatik.tu-muenchen.de> <50A728D8.2070105@rsise.anu.edu.au> <E20FDEC0-25AE-4C90-B51B-0510141A586B@cam.ac.uk> <50AABBDD.70700@rsise.anu.edu.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 20 Nov 2012, Jeremy Dawson wrote:

In a way, my first contribution to this thread was to make it clear thatboth "development" and "ordinary reasoning" are intertwined - there wasquite a lot of "development" involved in getting the right combinationof compound tactics and proof steps to avoid a proof script which wouldhave been 10000 lines long.

The bigger issue is that pen and paper proofs I do and publish in ajournal will be available as long as people want to read them. TheIsabelle proofs I do are in Isabelle 2005, and include theory and MLfiles from 1997, and so will in the future be inaccessible to anyone whodoesn't (or can't) install Isabelle 2005 (which only seems to work withone particular version of PolyML). Given the philosophy of Isabelledevelopers, prospective users need to be warned that if they want towrite proofs which will be accessible to future researchers, they needto be done in print.

Finally, it's worth pointing out that no one in this thread has actuallycome up with a suggestion about how to do the sort of proof which wasthe subject of my original post other than using Standard ML (which, Iunderstand, was designed for exactly that purpose).

Makarius

**References**:**[isabelle] Length of Proofs***From:*Jens Doll

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Makarius

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] syntax annotations
- Next by Date: Re: [isabelle] syntax annotations
- Previous by Thread: Re: [isabelle] Length of Proofs
- Next by Thread: Re: [isabelle] Length of Proofs
- Cl-isabelle-users November 2012 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