Am Donnerstag, den 10.03.2016, 11:00 +0100 schrieb Florian Haftmann:
> 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
Yes absolutely. I recently added by accident Lattice_Syntax somewhere
in the Library and a lot of AFP theories (and HOLCF) broke down at
unexpected places.
Alternatively: Would a lattice_syntax locale work nowadays? I remember
I tried it once and for some reason it didn't work. Either notations
aren't supported in locales or they are exported after the context
-block.
- Johannes
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
