changeset 63166 | 143f58bb34f9 |
parent 63165 | c12845e8e80a |
child 63173 | 3413b1cf30cd |
child 63178 | b9e1d53124f5 |
--- a/NEWS Thu May 26 15:31:04 2016 +0200 +++ b/NEWS Thu May 26 16:57:14 2016 +0200 @@ -93,9 +93,9 @@ *** Pure *** -* Code generator: config option "code_timinger" triggers -measurements of different phases of code generation. See -src/HOL/ex/Code_Timing.thy for examples. +* Code generator: config option "code_timing" triggers measurements of +different phases of code generation. See src/HOL/ex/Code_Timing.thy for +examples. *** HOL ***