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



For Isabelle 2005, just use the included documentation. I hope that it is reasonably complete.

You will find lots of useful “read" functions in the files sign.ML and thm.ML.
Larry

On 5 Dec 2010, at 10:43, <mark at proof-technologies.com> <mark at proof-technologies.com> wrote:

> on 28/11/10 8:54 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
>> 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
> 
> I see, so would I be right in saying that the "read" function is the
> appropriate ML function for parsing a string into a HOL term?  Is there a
> corresponding function for HOL types?  And where is the best place to find a
> complete description of the lex/syntax of Isabelle HOL terms and types (for
> Isabelle 2005)?






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