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.
Larry Paulson On 28 Sep 2021, 11:19 +0100, Kevin Kappelmann <[email protected]>, 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.
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
