> 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.haftm...@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-...@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
