*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] How do I do stone age interaction?*From*: <mark at proof-technologies.com>*Date*: Mon, 06 Dec 2010 15:40:56 +0000*Reply-to*: mark at proof-technologies.com

on 6/12/10 2:32 PM, Makarius <makarius at sketis.net> wrote: > There is also a lot of confusion here, because Isabelle2005 features about > 2 or 3 versions of basic things like syntax layers, goal modules etc. > The "read" function is an odd leftover from much earlier times. > > If you really want to learn about "stone age" Isabelle, I recommend > something like Isabelle98, or even 89. If you want to learn about current > Isabelle, then use the current release Isabelle2009-2. The > impracticability of using the raw ML loop in contemporay Isabelle is not > accidental, but an integral part of the system. By dropping out of it, > you won't learn the most important things. Hmm, not sure whether you're understanding my requirements fully. When I say "stone age", I don't mean "early version". What I mean is "basic ML toplevel interaction, like what exists in other classic LCF-style theorem provers, such as HOL90, HOL4, ProofPower HOL, HOL Light". So can I do this in Isabelle2005? If so, I'd like to, because this is closer to the contemporary system than Isabelle98. Please understand that I am not coming at this as a normal user - I am looking to understand the basic Isabelle HOL system itself, rather than to understand how to use advanced Isabelle HOL most effectively to perform proofs. To do this I will be examining Isabelle source code and interacting with the ML top level, constructing and/or parsing terms and types, examining how they get pretty printed, applying basic inference rules and writing my own basic inference rules. I imagine that interacting with Proof General, Isar, etc involves various layers of processing. What I want is to interact with the basic system, avoiding these layers (but still being able to parse/print expressions). By the way, I am getting somewhere on all of this by reading "Isabelle Logics: HOL" (referred to but not included in the Isabelle2005 documentation), and by using "read" (if there is a more appropriate way to parse HOL expressions in the ML toplevel, please tell me how). I have a description of the syntax in the above document, but there appears to be no detailed description of the lex. Mark

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

- Previous by Date: Re: [isabelle] Question on hypothesis
- Next by Date: Re: [isabelle] How do I do stone age interaction?
- 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