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

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.

Mark.

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





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