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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
