[isabelle-dev] Syntax for lattice operations?
florian.haftmann at informatik.tu-muenchen.de
Thu Mar 10 11:13:29 CET 2016
> 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.
>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 836 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev