[isabelle-dev] Normalise theorem wrt an environment

Makarius makarius at sketis.net
Wed Sep 29 12:41:44 CEST 2021

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.

(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.)


More information about the isabelle-dev mailing list