[isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

> What would be the objective of this change?

Mainly to get rid of those brittle (no_)notation declarations scattered
over various theories.  Organizing syntax through library theories does
not quite work out.

	Florian

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

-- 

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160310/1edc4b90/attachment.sig>