author | wenzelm |
Thu, 26 May 2016 16:57:14 +0200 | |
changeset 63166 | 143f58bb34f9 |
parent 63165 | c12845e8e80a |
child 63167 | 0909deb8059b |
--- 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 ***