Refurbishing the old ref manual in sunny Sicily recently, I've come across
the following tidbit, which is now updated in Isabelle/c5cc24781cbf for
the isar-ref manual:
\item Higher-order patterns in the sense of \cite{nipkow-patterns}.
These are terms in @{text "\<beta>"}-normal form (this will
always be the case unless you have done something strange) ...
^^^^^^^
This was probably written by Tobias about 20 years ago, in the heroic
times when the advanced higher-order rewriting engine was implemented.
So beta redexes within rewrite rules are considered "strange". From
empirical observations in the past 10 years, I can confirm that they are
also "strange" in the terms being simplified, and in other situations as
well.
One can put a filter before things like rewrite_conv to smash incoming
redexes, but it is futile to make non-normal terms the general rule. Many
other tools will suddenly become "broken" by such a "fix".
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
