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