[isabelle-dev] Syntax for lattice operations?
nipkow at in.tum.de
Sun Mar 13 13:55:31 CET 2016
On 10/03/2016 11:00, Florian Haftmann wrote:
> Hi all,
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow use of that quite generic
> notation for unforeseen applications.
> Meanwhile however all those operations to which that syntax is attached
> to are members of syntactic type classes. It could be worth to attempt
> to make that syntax standard, using funny subscripts or similar for the
> more exotic cases.
Florian, what are the more exotic cases?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev