ANNOUNCE
changeset 11109 ce1cefc6c14c
parent 11108 43791f99d71e
child 11600 bbd6268e0b4b
     1.1 --- a/ANNOUNCE	Tue Feb 13 16:05:56 2001 +0100
     1.2 +++ b/ANNOUNCE	Tue Feb 13 16:31:18 2001 +0100
     1.3 @@ -12,22 +12,22 @@
     1.4    * Poly/ML 4.0 used by default
     1.5      More robust, less disk space required.
     1.6  
     1.7 -  * Pure/Simplifier (Stefan Berghofer)
     1.8 +  * Simplifier (Stefan Berghofer)
     1.9      Proper implementation as a derived rule, outside the kernel!
    1.10  
    1.11 +  * Improved document preparation (Markus Wenzel)
    1.12 +    Near math-mode, sub/super scripts, more symbols etc.
    1.13 +
    1.14    * Isabelle/Isar (Markus Wenzel)
    1.15      Numerous usability improvements, e.g. support for initial
    1.16      schematic goals, failure prediction of subgoal statements,
    1.17      handling of non-atomic statements in induction.
    1.18  
    1.19 -  * Improved document preparation (Markus Wenzel)
    1.20 -    Near math-mode, sub/super scripts, more symbols etc.
    1.21 -
    1.22    * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    1.23        Thomas M Rasmussen, Markus Wenzel)
    1.24      A collection of generic theories to be used together with main HOL.
    1.25  
    1.26 -  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and Lawrence C Paulson)
    1.27 +  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
    1.28      General cleanup, more on nonstandard real analysis.
    1.29  
    1.30    * HOL/Unix (Markus Wenzel)