Email Gateway (Aug 22 2022 at 11:06): Email Gateway (Aug 22 2022 at 11:06):From: Peter Lammich <lammich@in.tum.de>
Hi,
I just had to learn that the named_theorems command introduced
"a subtle change of semantics due to external visual order vs. internal
reverse order" [NEWS].
What is the rationale behind this change?
The most common case where I use named_theorems, I want to be able to
later "overwrite" rules that have been declared previously, to allow for
a modular style of theory development. However, the new ordering of
named_theorems, and the ordering in which methods like "rule" or "subst"
try the rules do no longer allow for such a modular development, as the
oldest rules will always be tried first.
For my applications, this change means that I cannot use named_theorems
at all in many cases.
Email Gateway (Aug 22 2022 at 11:06):From: Lars Noschinski <noschinl@in.tum.de>
The new named_theorems allow you to add more general rules later on. In
practice, I always encountered the same case as Peter: I wanted to add
more specialized rules.
-- Lars
Last updated: Apr 26 2024 at 20:16 UTC