[isabelle-dev] Syntax for lattice operations?

[Lawrence Paulson]

What would be the objective of this change?
Larry

> On 10 Mar 2016, at 10:00, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> 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.
> 
> Cheers,
> 	Florian
> 
> --