[isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160310/1e18920f/attachment.asc>