For the final record:
Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1
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
Your workaround merely helps users of Group, not of Complete_Lattice.
Moreover, it doesn't make sense that Complete_Lattice imports Group, and
that the structure theorem about subgroups is now in lattice theory.
I request you revert this patch.
isabelle-dev mailing list