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?


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

> The you should study the "implementation" manual, although it is still
> only half through the main concepts.  Again see
> It also tells you about datatypes for types and terms etc.
> Makarius

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

> Probably you should look at the papers at
> 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.