[isabelle-dev] beta redexes

[Makarius]

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