[isabelle-dev] Syntax for lattice operations?

[Tobias Nipkow]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160313/80a4c15b/attachment.bin>