added list comprehension syntax
authorhaftmann
Sat Oct 27 12:48:24 2007 +0200 (2007-10-27)
changeset 2521348a1e80f5cdb
parent 25212 9dd61cb753ae
child 25214 91730b492a45
added list comprehension syntax
ANNOUNCE
     1.1 --- a/ANNOUNCE	Fri Oct 26 22:10:44 2007 +0200
     1.2 +++ b/ANNOUNCE	Sat Oct 27 12:48:24 2007 +0200
     1.3 @@ -27,14 +27,16 @@
     1.4  
     1.5  * New 'class' package combination of axclass + locale interpretation.
     1.6  
     1.7 +* Built-in Metis prover, external linkup for automated provers, and
     1.8 +'sledghammer' command for automated proof synthesis.
     1.9 +
    1.10 +* Full list comprehension syntax.
    1.11 +
    1.12  * Various improvements in locale infrastructure (interpretation etc.)
    1.13  
    1.14  * Various improvements of Isar language elements and related proof
    1.15  tools.
    1.16  
    1.17 -* Built-in Metis prover, external linkup for automated provers, and
    1.18 -'sledghammer' command for automated proof synthesis.
    1.19 -
    1.20  * Second generation code-generator for a subset of HOL, targeting SML,
    1.21  Haskell, and OCaml.
    1.22