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

Clemens Ballarin ballarin at in.tum.de
Fri Sep 1 10:29:01 CEST 2017

> On 2017-08-24 09:38, Thiemann, Rene wrote:
>>   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.

I have done so now.  I also restored the original import order.


More information about the isabelle-dev mailing list