[isabelle-dev] Nominal and FinFuns from the AFP
makarius at sketis.net
Thu May 31 10:53:30 CEST 2012
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.
More information about the isabelle-dev