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