1.1 --- a/NEWS Wed Aug 03 14:24:23 2011 +0200
1.2 +++ b/NEWS Wed Aug 03 16:08:02 2011 +0200
1.3 @@ -98,9 +98,11 @@
1.4 - theory Library/Code_Char_ord provides native ordering of characters
1.5 in the target language.
1.6 - commands code_module and code_library are legacy, use export_code instead.
1.7 - - evaluator "SML" and method evaluation are legacy, use evaluator "code"
1.8 - and method eval instead.
1.9 -
1.10 + - method evaluation is legacy, use method eval instead.
1.11 + - legacy evaluator "SML" is deactivated by default. To activate it, add the following
1.12 + line in your theory:
1.13 + setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}
1.14 +
1.15 * Declare ext [intro] by default. Rare INCOMPATIBILITY.
1.16
1.17 * Nitpick: