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.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
