NEWS
authorbulwahn
Mon Jul 25 10:42:32 2011 +0200 (2011-07-25)
changeset 4395764f88ef1835e
parent 43956 4611af362cd0
child 43958 bc5e767f0f46
NEWS
NEWS
     1.1 --- a/NEWS	Mon Jul 25 10:40:52 2011 +0200
     1.2 +++ b/NEWS	Mon Jul 25 10:42:32 2011 +0200
     1.3 @@ -93,7 +93,10 @@
     1.4  * Code generation:
     1.5    - theory Library/Code_Char_ord provides native ordering of characters
     1.6      in the target language.
     1.7 -    
     1.8 +  - commands code_module and code_library are legacy, use export_code instead. 
     1.9 +  - evaluator "SML" and method evaluation are legacy, use evaluator "code"
    1.10 +    and method eval instead.
    1.11 +  
    1.12  * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
    1.13  
    1.14  * Nitpick:
    1.15 @@ -132,6 +135,8 @@
    1.16      It requires that the Glasgow Haskell compiler is installed and
    1.17      its location is known to Isabelle with the environment variable
    1.18      ISABELLE_GHC.
    1.19 +  - Removed quickcheck tester "SML" based on the SML code generator
    1.20 +    from HOL-Library
    1.21  
    1.22  * Function package: discontinued option "tailrec".
    1.23  INCOMPATIBILITY. Use partial_function instead.