ANNOUNCE
changeset 12996 7ac0a7e306db
parent 12995 d9da3015aab4
child 12999 8ad8d02b973f
equal deleted inserted replaced
12995:d9da3015aab4 12996:7ac0a7e306db
    38     operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
    38     operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
    39 
    39 
    40   * HOL/Bali: large application concerning formal treatment of Java.
    40   * HOL/Bali: large application concerning formal treatment of Java.
    41     (by David von Oheimb and Norbert Schirmer).
    41     (by David von Oheimb and Norbert Schirmer).
    42 
    42 
    43   * HOL/Hoare_Parallel: large application concerning verification of
    43   * HOL/HoareParallel: large application concerning verification of
    44     parallel imperative programs (Owicki-Gries method etc.)
    44     parallel imperative programs (Owicki-Gries method, Rely-Guarantee
       
    45     method, verification examples: garbage collection, mutual
       
    46     exclusion, etc.)
    45     (by Leonor Prensa Nieto).
    47     (by Leonor Prensa Nieto).
    46 
    48 
    47   * HOL/GroupTheory: group theory examples including Sylow's theorem
    49   * HOL/GroupTheory: group theory examples including Sylow's theorem
    48     (by Florian Kammüller).
    50     (by Florian Kammüller).
    49 
    51