ANNOUNCE
changeset 25271 f28efd37e18a
parent 25259 8d6b03eef9c9
child 25305 574c4964fe54
equal deleted inserted replaced
25270:2ed7b34f58e6 25271:f28efd37e18a
     5 
     5 
     6 This release introduces fundamental changes over Isabelle2005, see the
     6 This release introduces fundamental changes over Isabelle2005, see the
     7 NEWS file in the distribution for more details.  Numerous existing
     7 NEWS file in the distribution for more details.  Numerous existing
     8 concepts have been generalized and re-implemented based on novel
     8 concepts have been generalized and re-implemented based on novel
     9 system architecture.  New theories and proof tools have been added
     9 system architecture.  New theories and proof tools have been added
    10 (mostly for HOL).
    10 (mostly for HOL).  Some highlights are:
    11 
       
    12 The main highlights are:
       
    13 
    11 
    14 * Support for nominal datatypes (binding structures) due to the
    12 * Support for nominal datatypes (binding structures) due to the
    15 HOL-Nominal logic.
    13 HOL-Nominal logic.
    16 
    14 
    17 * General local theory infrastructure for specifications depending on
    15 * General local theory infrastructure for specifications depending on
    31 'sledgehammer' command for automated proof synthesis.
    29 'sledgehammer' command for automated proof synthesis.
    32 
    30 
    33 * Second generation code generator for a subset of HOL, targeting SML,
    31 * Second generation code generator for a subset of HOL, targeting SML,
    34 Haskell, and OCaml.
    32 Haskell, and OCaml.
    35 
    33 
    36 * Command 'normal_form' and method 'normalization'
    34 * Embedding of ML code into theories with static references to the
    37 for evaluating terms with free variables.
    35 logical context (via antiquotations).
    38 
    36 
    39 * Full list comprehension syntax.
    37 * Command 'normal_form' and method "normalization" for evaluating
       
    38 terms with free variables.
       
    39 
       
    40 * Full list comprehension syntax for HOL.
       
    41 
       
    42 * Much improved algebraic capabilities, including Groebner bases.
    40 
    43 
    41 * Parallel loading of theories based on native multicore support in
    44 * Parallel loading of theories based on native multicore support in
    42 Poly/ML 5.1.
    45 Poly/ML 5.1.
    43 
       
    44 * Much improved algebraic capabilities, including Groebner bases.
       
    45 
    46 
    46 
    47 
    47 You may get Isabelle2007 from the following mirror sites:
    48 You may get Isabelle2007 from the following mirror sites:
    48 
    49 
    49   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
    50   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/