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.

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

Reply via email to