# [isabelle-dev] beta redexes

Makarius makarius at sketis.net
Tue Nov 20 16:28:19 CET 2012

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