[isabelle-dev] Method parsing, YXML and term construction.

2010-02-09 Thread Makarius
On Tue, 9 Feb 2010, Thomas Sewell wrote: Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem to be my friends. In fact, I sort of wish I'd known about them earlier. I remember in one of the record package proofs it was annoying me that I had to construct the types

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-08 Thread Florian Haftmann
Hi Thomas, Isabelle internalizes expressions in two steps: (1) parse :: raw string (type string) - raw term (type term) (2) check :: raw term (type term) - internalized term with types inferred etc. (type term) It seems to me that most things you want to do can be done using (2)

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-08 Thread Makarius
On Mon, 8 Feb 2010, Thomas Sewell wrote: Specifically, f is a polymorphic constant, x is a simple function application generated by our ML code, and y is supplied by the user and must be parsed. So far, our code has simply generated the string expression f (x) (y) and passed it to

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-08 Thread Thomas Sewell
Hello to isabelle-dev. Suppose some ML code I wrote has terms f, x and y. I'd like to be able to produce the function application f x y with the catch that f, x and y may all have type parameters that need to be adapted to each other. Is there any convenient facility for doing this in Isabelle