# [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

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


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.


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.

Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev