ANNOUNCE
changeset 11108 43791f99d71e
parent 11062 e86340dc1d28
child 11109 ce1cefc6c14c
equal deleted inserted replaced
11107:09879d39b3f5 11108:43791f99d71e
    25 
    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 (Lawrence C Paulson and Jacques Fleuriot)
    30   * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and 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.