*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Length of Proofs*From*: Makarius <makarius at sketis.net>*Date*: Thu, 22 Nov 2012 14:12:26 +0100 (CET)*Cc*: Jeremy Dawson <jeremy at rsise.anu.edu.au>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <04665034-67AE-4672-9101-A05F7AA8C385@cam.ac.uk>*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> <04665034-67AE-4672-9101-A05F7AA8C385@cam.ac.uk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 22 Nov 2012, Lawrence Paulson wrote:

You still have the capacity to code your own proof procedures; ML isjust one level down. And you get a much more readable proof language.

In general Isar vs. its embedded languages works like this: * Isar is the main framework of Isabelle to integrate many other languages. * The Isar languages for specifications (e.g. 'theorem', 'definition', 'function') and proofs (e.g. 'fix', 'assume', 'show' ...) are the primary applications of the Isar framework. * The logical language (Pure types/terms/propositions with specific HOL notation) is another important embedded language, cf. the quotes that have been around this language even in the ancient ML-only times of Isabelle in the 1990-ies. * ML is embedded into Isar in a similar manner, but at the same time it is the implementation language of Isar. Moreover, ML quoted inside Isar can antiquote logic/Isar expressions. So the image for that is http://en.wikipedia.org/wiki/File:Yin_and_Yang.svg

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

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

- Previous by Date: Re: [isabelle] Length of Proofs
- Next by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- 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