Re: [isabelle] How do I do stone age interaction?



Jeremy, thanks for the reply.

on 6/12/10 6:10 PM, Jeremy Dawson <jeremy at rsise.anu.edu.au> wrote:
> On 06/12/10 16:19, Makarius wrote:
>> On Mon, 6 Dec 2010, mark at proof-technologies.com wrote:

> You can certainly do ML interaction effectively in Isabelle2005 - it's
> the way I normally use Isabelle.

Hmm.  I'll carry on looking into Isabelle2005 too then.

> The ML layer certainly helps you perform proofs effectively - just by
> way of example here is something I wrote this afternoon, which I
> understand cannot be done in Isar
>
> fun in_tac sg st = (rtac insertI1 ORELSE' (rtac insertI2 THEN' in_tac))
> sg st ;
>
> ....

Excellent, thanks.

>> Dropping out of the Isar loop, you won't see anything of the HOL name
>> space, and thus cannot use Isabelle/HOL.
>
> I'm not sure if I understand this right, but at the ML level I certainly
> get all the HOL syntax and theorems - note, though, if you're using
> "new-style" theory files, then to get theorems derived from the theory
> file as ML identifiers you need to use the "use_legacy_bindings" function.

Yes, so do I...  Maybe they are talking about Isabelle2009-2?

> I don't recall from earlier emails in this thread whether you actually
> have got Isabelle2005 running.  As far as I can see it requires an old
> version of PolyML - namely 4.1.4.  I don't know whether that is easily
> available now, but I can give you a copy (for x86_linux) if required.

Thanks for the offer, but I have already managed to install Isabelle2005
(with Poly/ML 4.1.4) and Isabelle2009 (with Poly/ML 5.2.1) from source.  I'm
now building Isabelle 2009-2 (with Poly/ML 5.2.1) from source.

Incidentally, Isabelle2005 required a few source code changes to get it
through Poly/ML 4.1.4.  This seems strange to me, and sounds like a
configuration management problem with either the precise version of
Isabelle2005 or the precise version of Poly/ML 4.1.4 source code that
appears on the web.  I can provide details of the changes required if anyone
is interested..

Mark.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.