[isabelle-dev] Towards the Isabelle2017 release
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 24 17:34:23 CEST 2017
> - 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev