[isabelle-dev] Method parsing, YXML and term construction.
urbanc at in.tum.de
Tue Feb 9 16:50:25 CET 2010
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
More information about the isabelle-dev