changeset 43712 | 0e594ba0b324 |
parent 43686 | 61668e617a3b |
child 43743 | f115492c7c8d |
1.1 --- a/NEWS Wed May 18 15:45:33 2011 +0200 1.2 +++ b/NEWS Wed May 18 15:45:34 2011 +0200 1.3 @@ -58,6 +58,10 @@ 1.4 1.5 *** HOL *** 1.6 1.7 +* Code generation: 1.8 + - theory Library/Code_Char_ord provides native ordering of characters 1.9 + in the target language. 1.10 + 1.11 * Declare ext [intro] by default. Rare INCOMPATIBILITY. 1.12 1.13 * Finite_Set.thy: locale fun_left_comm uses point-free characterisation;