NEWS

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