[isabelle-dev] Normalise theorem wrt an environment
lp15 at cam.ac.uk
Wed Sep 29 12:36:56 CEST 2021
Thanks for the suggestion and code. I wonder however how common it is to normalise a theorem wrt an environment. Environments are an internal data structure largely tied up with unification and not used to that much outside the kernel.
On 28 Sep 2021, 11:19 +0100, Kevin Kappelmann <kevin.kappelmann at tum.de>, wrote:
I see that there are functions to normalise a type (Envir.norm_type) and
a term (Envir.norm_term) wrt an environment. Is there also a function to
normalise a theorem wrt an environment? If not, I think doing such a
normalisation is very common and should be added to Isabelle/Pure.
Attached, find my proposal for such a function (norm_thm) and some
examples why a simpler alternative (that is akin to the function
described in the Isabelle/ML cookbook [1, page 57]) does not work. The
file compiles using the current Isabelle development version.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev