*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Length of Proofs*From*: Makarius <makarius at sketis.net>*Date*: Thu, 22 Nov 2012 13:42:23 +0100 (CET)*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50AD562E.5090103@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> <98A92B35-BD03-4E31-B0E5-BBD552920CF6@cam.ac.uk> <50AC4179.7070101@rsise.anu.edu.au> <49EAB30D-6FC1-4B09-A576-12094F24F98A@cam.ac.uk> <50AD562E.5090103@rsise.anu.edu.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 22 Nov 2012, Jeremy Dawson wrote:

Given that in HOL (as in Isabelle, both pre and post Isar) one canalways use proof procedures coded by someone else, this seems to sum upto saying that Isabelle/Isar is like HOL, minus the capacity to codeone's own proof procedures, plus -- what ??

From where did you get the "minus"? Certainly not from this thread, where

Makarius

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

**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

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

**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] Length of Proofs
- Next by Date: Re: [isabelle] Length of Proofs
- 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