On 10/03/16 11:19, Makarius wrote: > On Thu, 10 Mar 2016, Johannes Hölzl wrote: > >> 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. > > The concept of 'bundle' was introduced for that, e.g. to allow "includes > lattice_syntax" for local contexts. > > Unfortunately, it is not quite finished: notation within bundles is not > yet supported. It might be relatively easy to do that, but I am > presently working in other corners of the system.
This thread is still pending, while the bundle concept has been enhanced
in Isabelle/a59801b7f125.
One extra complication for Lattice_Syntax.thy (in contrast to
FinFun.thy) is the use of raw 'syntax' declarations, which are not
localized and thus cannot be put into bundles. (There might be other
ways to do that.)
I have also started an experiment to keep INF and SUP symbol syntax in
main HOL and eliminate clashes in the applications. In the middle of
that I kept all of Lattice_Syntax.thy and eliminated clashes of "inf"
and "sup" syntax as well. The resulting changesets are included.
This shows changes are only needed in relatively isolated places so
far there was not even any attempt to use the more flexible type class
operations of main HOL instead of independent operations with
alternative (bold) syntax.
How shall we proceed? Make Lattice_Syntax standard and cleanup
conflicting applications?
Makarius
ch-lattice_syntax1.gz
Description: application/gzip
ch-lattice_syntax2.gz
Description: application/gzip
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
