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

[Christian Urban]

Thomas Sewell writes:
 > 
 > BTW, should I have known this already? Is there some part of the
 > documentation that I should have read, but have overlooked?

Sort of. Both functions are used in an example in the Programming 
Tutorial[*] on page 19. What the function check_term does is a bit 
more carefully described on page 52. But for the usage you have
in mind there is only a stub (since a long time ago) on page 92.
I just have not come around of writing this part yet. Help is of 
course very much appreciated. I think what you asked is a "common
idom" in Isabelle and there are bound to be others that will trip 
over this.

Christian


[*] http://isabelle.in.tum.de/nominal/activities/idp/