[isabelle-dev] Repaired Card_Equiv_Relations
Hi, for some reason, Lukas' entry Card_Equiv_Relations broke and remains broken. Since I wasn't sure anyone was taking care of it, I pushed 4d10819509 to afp-testboard to rectify the issue. I'm writing this to avoid duplicate work. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS
Code generator: config option "code_timinger" triggers measurements of different phases of code generation. See src/HOL/ex/Code_Timing.thy for examples. This enables a canonical way to examine performance of generated code and corresponding computations on different levels. In the process of implementing this a few more steps where done to eliminate occurences of theory background certificates and a few closures have been corrected which might be the reason for reported unplausible timing behaviour of computations relying on the code generator. 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