[isabelle-dev] Nominal and FinFuns from the AFP

Lawrence Paulson lp15 at cam.ac.uk
Sun May 13 11:07:38 CEST 2012


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).

More information about the isabelle-dev mailing list