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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev