[isabelle-dev] Normalise theorem wrt an environment

[Makarius]

On 29/09/2021 12:36, Lawrence Paulson wrote:
> 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.

This is true. Even worse there is a second use for matching, with slightly
different meaning of the same data structure. We have a "Paulson regime" and a
"Nipkow regime" here, from the depths of time of Isabelle development (approx.
1990).

(I did not find time to look at the cookbook example yet. It is de-facto
fan-fiction with relatively little relevance to Isabelle sources and development.)


	Makarius