[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 31 13:57:20 CEST 2017
>> If one imports HOL-Algebra.Multiplicative_Group (which we actually do
>> via some transitive import), then \mu (LFP), \nu (GFP) and
>> \phi (Euler’s totient function) become constants.
> Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.
sorry, I didn't recognize your follow-up message to this thread until now.
Of course you are free to go ahead and revert the workaround e.g. using
hg backout 5a42eddc11c1
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev