ANNOUNCE
changeset 25306 351ca94cabdb
parent 25305 574c4964fe54
child 27005 739d239ba514
equal deleted inserted replaced
25305:574c4964fe54 25306:351ca94cabdb
    26 * New 'class' package combination of axclass + locale interpretation.
    26 * New 'class' package combination of axclass + locale interpretation.
    27 
    27 
    28 * Built-in Metis prover, external linkup for automated provers, and
    28 * Built-in Metis prover, external linkup for automated provers, and
    29 'sledgehammer' command for automated proof synthesis.
    29 'sledgehammer' command for automated proof synthesis.
    30 
    30 
    31 * Autoquickcheck: lemmas are tested for counterexamples
    31 * Auto quickcheck: toplevel goals are tested for counterexamples
    32 automatically when they are stated. 
    32 automatically when they are stated.
    33 
    33 
    34 * Second generation code generator for a subset of HOL, targeting SML,
    34 * Second generation code generator for a subset of HOL, targeting SML,
    35 Haskell, and OCaml.
    35 Haskell, and OCaml.
    36 
       
    37 * Embedding of ML code into theories with static references to the
       
    38 logical context (via antiquotations).
       
    39 
    36 
    40 * Command 'normal_form' and method "normalization" for evaluating
    37 * Command 'normal_form' and method "normalization" for evaluating
    41 terms with free variables.
    38 terms with free variables.
    42 
    39 
    43 * Full list comprehension syntax for HOL.
    40 * Full list comprehension syntax for HOL.
    44 
    41 
    45 * Much improved algebraic capabilities, including Groebner bases.
    42 * Much improved algebraic capabilities, including Groebner bases.
       
    43 
       
    44 * Embedding of ML code into theories with static references to the
       
    45 logical context (via antiquotations).
    46 
    46 
    47 * Parallel loading of theories based on native multicore support in
    47 * Parallel loading of theories based on native multicore support in
    48 Poly/ML 5.1.
    48 Poly/ML 5.1.
    49 
    49 
    50 
    50