Hi Clemens, >>> Concerning \mu and \nu, I am currently investigating whether an import >>> swap could re-establish the situation known from Isabelle2016-1 >> >> see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1
> I had overlooked that \mu and \nu are global constants when importing > this material, which I had received from Simon Foster. This needs to be > addressed properly. I did have a look at the overall situation but IMHO there are too many open ends which cannot be resolved before the upcoming release: * »no_notation« would mess up the material considerably and is difficult to place: traditionally, HOL-Algebra has no universal entry point which is guaranteed to be imported after all other theories. * Specific syntax could be placed into bundles, but this cannot be done incrementally. * Giving up \mu and \nu and coming up with an alternative syntax. * … Each of these requires subtantial thinking and appears much too invasive to me. > Your workaround merely helps users of Group, not of Complete_Lattice. That is the relevant point for the upcoming release: users of Group in Isabelle2016-1 (and there are many, since Group is used in substantial parts of both distribution of AFP) need not to worry about additional syntactic artefacts in Isabelle2017 either; Complete_Lattice is new in Isabelle2017 and does not induce any regression problems. > Moreover, it doesn't make sense that Complete_Lattice imports Group, and > that the structure theorem about subgroups is now in lattice theory. The theorem in question requires both the notion of subgroup and complete lattices, hence the import order dictates in which theory the theorem has to reside (btw. the current import order is similar to HOL-Main where Complete_Lattices comes after Groups). When placing it, I followed the pre-existing textual reference (http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1#l1.16). I am happy to add the symmetric textual reference to Group.thy if this clarifies the situation. 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
