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 ;
>> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and