From: Fabian Huch <huch@in.tum.de>
I find it unexpected that lattice_syntax is disabled by default, as I
would consider lattices quite the canonical structure. Given that it is
pretty simple to turn the syntax back off (unbundle no_lattice_syntax),
would it make sense to have it active by default? In my experience, less
experienced users frequently stumble over that.
The counter-argument is that quite a few AFP entries (~50) define their
own symbols (mostly bottom/top), and to turn it off, one has to unbundle
the no_lattice_syntax for every import from a foreign session.
Fabian
From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
For what it's worth, my two cents are that global notation, and global interpretations,
are inherently evil. This is much the same as my feeling about global structure definitions
in Standard ML, as opposed to functors that can be used to instantiate the structures in
the context in which they are required.
From: Tobias Nipkow <nipkow@in.tum.de>
I would agree, for exactly the counter-argument Fabian gave himself.
Tobias
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC