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/
