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



Note that in the early days, there was no form of antiquotation. You could create a term by parsing the corresponding string or (painfully) using constructor functions.
Larry

On 28 Nov 2010, at 14:32, <mark at proof-technologies.com> <mark at proof-technologies.com> wrote:

> 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?






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