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? Tobias
Cheers,
Florian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
