Hi Makarius, Am 11.06.2016 um 00:13 schrieb Makarius: > 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.
first, thanks for implementing this; we can now really move forward wrt. more flexible syntax. > 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? I had a quick look at the changesets; as far as I can glimpse, most occurences are due to LUB from HOLCF/Porder.thy. For the moment I think bold syntax in the first choice. In the middle run I would suggest to have a closer look at HOLCF/Porder.thy to see whether something can be done to integrate it more with the standard type classes; a least it formalizes a lot about upper / lower bounds which is not HOLCF-specific in any way, so it could go to HOL/Library for example. There are various occurences of no_notation etc. in the HOL and AFP theories which I will inspect to see what can be done there. Cheers, Florian -- 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