*To*: mark at proof-technologies.com*Subject*: Re: [isabelle] How do I do stone age interaction?*From*: Makarius <makarius at sketis.net>*Date*: Mon, 6 Dec 2010 17:19:56 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1291650056496@names.co.uk>*References*: <1291650056496@names.co.uk>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Mon, 6 Dec 2010, mark at proof-technologies.com wrote:

on 6/12/10 2:32 PM, Makarius <makarius at sketis.net> wrote:The impracticability of using the raw ML loop in contemporay Isabelleis not accidental, but an integral part of the system. By dropping outof it, you won't learn the most important things.Hmm, not sure whether you're understanding my requirements fully. WhenI say "stone age", I don't mean "early version". What I mean is "basicML toplevel interaction, like what exists in other classic LCF-styletheorem provers, such as HOL90, HOL4, ProofPower HOL, HOL Light". Socan I do this in Isabelle2005? If so, I'd like to, because this iscloser to the contemporary system than Isabelle98.Please understand that I am not coming at this as a normal user - I amlooking to understand the basic Isabelle HOL system itself, rather thanto understand how to use advanced Isabelle HOL most effectively toperform proofs. To do this I will be examining Isabelle source code andinteracting with the ML top level, constructing and/or parsing terms andtypes, examining how they get pretty printed, applying basic inferencerules and writing my own basic inference rules. I imagine thatinteracting with Proof General, Isar, etc involves various layers ofprocessing. What I want is to interact with the basic system, avoidingthese layers (but still being able to parse/print expressions).

By the way, I am getting somewhere on all of this by reading "IsabelleLogics: HOL" (referred to but not included in the Isabelle2005documentation), and by using "read" (if there is a more appropriate wayto parse HOL expressions in the ML toplevel, please tell me how). Ihave a description of the syntax in the above document, but thereappears to be no detailed description of the lex.

Makarius

**Follow-Ups**:**Re: [isabelle] How do I do stone age interaction?***From:*Jeremy Dawson

**References**:

- Previous by Date: Re: [isabelle] How do I do stone age interaction?
- Next by Date: [isabelle] Suppressing warnings
- Previous by Thread: Re: [isabelle] How do I do stone age interaction?
- Next by Thread: Re: [isabelle] How do I do stone age interaction?
- Cl-isabelle-users December 2010 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