[isabelle-dev] Towards the Isabelle2017 release
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 24 17:34:23 CEST 2017
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>
More information about the isabelle-dev
mailing list