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). _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
