ANNOUNCE
changeset 25213 48a1e80f5cdb
parent 25197 7a169cfda866
child 25228 59afe8a0a7e1
equal deleted inserted replaced
25212:9dd61cb753ae 25213:48a1e80f5cdb
    25 
    25 
    26 * New 'function' package for general recursive function definitions.
    26 * New 'function' package for general recursive function definitions.
    27 
    27 
    28 * New 'class' package combination of axclass + locale interpretation.
    28 * New 'class' package combination of axclass + locale interpretation.
    29 
    29 
       
    30 * Built-in Metis prover, external linkup for automated provers, and
       
    31 'sledghammer' command for automated proof synthesis.
       
    32 
       
    33 * Full list comprehension syntax.
       
    34 
    30 * Various improvements in locale infrastructure (interpretation etc.)
    35 * Various improvements in locale infrastructure (interpretation etc.)
    31 
    36 
    32 * Various improvements of Isar language elements and related proof
    37 * Various improvements of Isar language elements and related proof
    33 tools.
    38 tools.
    34 
       
    35 * Built-in Metis prover, external linkup for automated provers, and
       
    36 'sledghammer' command for automated proof synthesis.
       
    37 
    39 
    38 * Second generation code-generator for a subset of HOL, targeting SML,
    40 * Second generation code-generator for a subset of HOL, targeting SML,
    39 Haskell, and OCaml.
    41 Haskell, and OCaml.
    40 
    42 
    41 * Improved support for arbitrary ML operations depending on the
    43 * Improved support for arbitrary ML operations depending on the