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



On 28/11/10 14:32, 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?
>
> Mark.
>   
Mark,

If I understand the question in your last sentence correctly, the
information you want is in the reference manual, sections 6.5 (terms)
and 6.8 (types, which are contained in terms).  (this is applies to the
Isabelle2005 reference manual - it may have been changed since).

../Isabelle2005/doc/ref.dvi

Jeremy






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