Hi Clemens, >> 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
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
