ANNOUNCE
changeset 11109 ce1cefc6c14c
parent 11108 43791f99d71e
child 11600 bbd6268e0b4b
equal deleted inserted replaced
11108:43791f99d71e 11109:ce1cefc6c14c
    10 NEWS file distributed with Isabelle for more details.
    10 NEWS file distributed with Isabelle for more details.
    11 
    11 
    12   * Poly/ML 4.0 used by default
    12   * Poly/ML 4.0 used by default
    13     More robust, less disk space required.
    13     More robust, less disk space required.
    14 
    14 
    15   * Pure/Simplifier (Stefan Berghofer)
    15   * Simplifier (Stefan Berghofer)
    16     Proper implementation as a derived rule, outside the kernel!
    16     Proper implementation as a derived rule, outside the kernel!
       
    17 
       
    18   * Improved document preparation (Markus Wenzel)
       
    19     Near math-mode, sub/super scripts, more symbols etc.
    17 
    20 
    18   * Isabelle/Isar (Markus Wenzel)
    21   * Isabelle/Isar (Markus Wenzel)
    19     Numerous usability improvements, e.g. support for initial
    22     Numerous usability improvements, e.g. support for initial
    20     schematic goals, failure prediction of subgoal statements,
    23     schematic goals, failure prediction of subgoal statements,
    21     handling of non-atomic statements in induction.
    24     handling of non-atomic statements in induction.
    22 
    25 
    23   * Improved document preparation (Markus Wenzel)
       
    24     Near math-mode, sub/super scripts, more symbols etc.
       
    25 
       
    26   * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    26   * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    27       Thomas M Rasmussen, Markus Wenzel)
    27       Thomas M Rasmussen, Markus Wenzel)
    28     A collection of generic theories to be used together with main HOL.
    28     A collection of generic theories to be used together with main HOL.
    29 
    29 
    30   * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and Lawrence C Paulson)
    30   * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
    31     General cleanup, more on nonstandard real analysis.
    31     General cleanup, more on nonstandard real analysis.
    32 
    32 
    33   * HOL/Unix (Markus Wenzel)
    33   * HOL/Unix (Markus Wenzel)
    34     Some Aspects of Unix file-system security; demonstrates
    34     Some Aspects of Unix file-system security; demonstrates
    35     Isabelle/Isar in typical system modelling and verification tasks.
    35     Isabelle/Isar in typical system modelling and verification tasks.