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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
