NEWS
changeset 44023 3e5f8cc666db
parent 44019 ee784502aed5
child 44027 d01b3f045111
     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: