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



These documents I'm sure will be very useful, and Makarius's implementation
manual looks especially useful for my purposes.  But I also want to carry
out basic interaction - this is just the way I go about learning about the
innards of a system - I like to construct my own terms and experiment.  So
can I enter HOL term quotations in Isabelle 2005?  And can I use ML
constructor functions to create HOL terms?

Mark.

on 28/11/10 1:26 PM, Makarius <makarius at sketis.net> wrote:

> The you should study the "implementation" manual, although it is still
> only half through the main concepts.  Again see
> http://www4.in.tum.de/~wenzelm/test/implementation.pdf
>
> It also tells you about datatypes for types and terms etc.
>
> Makarius

on 28/11/10 1:42 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> Probably you should look at the papers at
> http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html
>
> Look particularly at the papers under the tab “of historical interest".
> Larry





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