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.

On 5 Dec 2010, at 10:43, <mark at> <mark at> wrote:

> on 28/11/10 8:54 PM, Lawrence Paulson <lp15 at> 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.