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



on 27/11/10 11:25 AM, Makarius <makarius at sketis.net> wrote:

> In order to be productive with Isabelle/ML you should build up your
> context in Isar source notation and the experiment with it via small ML
> snippets.  What is your application anyway?  Serious use of Isabelle
> outside the Isar system infrastructure is hard to imagine.

Unlike other users, I'm not aiming to use Isabelle for performing proofs as
such.  Rather I'm looking to gain a deep understanding of how Isabelle
works.  But thanks for the Isar example for Socrates, which will help me
understand Isar.

on 27/11/10 11:55 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> You might consider downloading an older version from here:
> http://www.cl.cam.ac.uk/~lp15/archive/
>
> Until around 2005, ML level interaction was still supported.

Thanks.  I've got Isabelle 2005 with HOL up and running now (curiously, this
required a handful of changes to the Isabelle ML source code to get it
through what purports to be Poly/ML 4.1.4).  But how do I enter HOL term and
type quotations into the session?  And what are the HOL term and type
constructor functions?

Mark.





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