[isabelle-dev] Nominal and FinFuns from the AFP

[Makarius]

On Sun, 13 May 2012, Florian Haftmann wrote:

> c) I strongly object to clutter the HOL syntax even more than now by 
> incorporating just another fancy syntax.  I would prefer the lattice 
> solution (delete syntax immediately after use and provide a library 
> theory to optionally include it later), or maybe it is also possible to 
> use context blocks for this (another nice case study).

This is indeed still the canonical solution to the syntax problem for 
library material, and I see it now in Isabelle/d60f6b41bf2d for FinFun.

At some point, when I have bundles ready to work with the existing 
notation commands, we can fine-tune this scheme further, to allow users to 
'include' syntax in local situations.


 	Makarius