Hi Rene,

> - In the NEWS I read about freeing short constant names like the
>   “Renamed ii to imaginary_unit in order to free up ii as a variable”.
>   I definitely support this kind of change, but at the same time found
>   quite the opposite in HOL-Algebra:
>   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.
>   This was a bit annoying.

thanks for pointing that out.

\phi is the result of a simple typo accident (cf.

I would still appreciate if someone would take the comment »Deviates
from the definition given in the library in number theory« as a starting
point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.

Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1

> - There have been some changes w.r.t. code-generation which now lead
>   to runtime exception in the generated code. For instance, now
>   I get code like
>   “f x = Code.abort …” 
>   whereas in 2016-1 there was a proper code like
>   “f x = some ordinary right-hand side” 
>   We did not yet isolate the problem and will report later.

OK, I will dig into this after you have isolated it.  Might be well that
this only occurs on certain theory merges.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to