[isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

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.
http://isabelle.in.tum.de/repos/testboard/rev/6c818fc0c817).

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
(http://isabelle.in.tum.de/repos/testboard/rev/0ad153ee9ece).

> - 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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170824/c7436ecb/attachment.sig>