changeset 63165 | c12845e8e80a |
parent 63161 | 2660ba498798 |
child 63166 | 143f58bb34f9 |
--- a/NEWS Thu May 26 15:27:50 2016 +0200 +++ b/NEWS Thu May 26 15:31:04 2016 +0200 @@ -91,6 +91,13 @@ Isabelle2016). INCOMPATIBILITY, use "standard" instead. +*** Pure *** + +* Code generator: config option "code_timinger" triggers +measurements of different phases of code generation. See +src/HOL/ex/Code_Timing.thy for examples. + + *** HOL *** * Probability/Random_Permutations.thy contains some theory about