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

2010-02-08 Thread Florian Haftmann
URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20100208/118a11b1/attachment.pgp

[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