Re: [isabelle] How do I do stone age interaction?
(apologies for a week of absence...)
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
on 29/11/10 10:24 AM, Jeremy Dawson <jeremy at rsise.anu.edu.au> wrote:
> 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).
That's one of the two things I was looking for. Thanks that helps.
> On 28/11/10 14:32, mark at proof-technologies.com wrote:
>> But I also want to carry out basic interaction - this is just the way I
>> 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