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 sketis.net> 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.
on 28/11/10 1:42 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Probably you should look at the papers at
> Look particularly at the papers under the tab “of historical interest".
This archive was generated by a fusion of
Pipermail (Mailman edition) and