[isabelle-dev] Repaired Card_Equiv_Relations

2016-05-26 Thread Lars Hupel
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

2016-05-26 Thread Florian Haftmann
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