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