Dear Florian,

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 addressed properly.

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

Reply via email to