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

Clemens Ballarin ballarin at in.tum.de
Fri Aug 25 09:33:12 CEST 2017

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



More information about the isabelle-dev mailing list