[isabelle-dev] Nominal and FinFuns from the AFP

[Lawrence Paulson]

Precisely.
Larry

On 13 May 2012, at 09:44, 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).