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