1.1 --- a/NEWS	Mon Aug 23 16:35:53 2004 +0200
     1.2 +++ b/NEWS	Mon Aug 23 16:41:06 2004 +0200
     1.3 @@ -215,6 +215,9 @@
     1.4    INCOMPATIBILITY: old proofs break occasionally as simplification may
     1.5    now solve more goals than previously.
     1.6  
     1.7 +* HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
     1.8 +  (containing Boolean satisfiability problems) into Isabelle/HOL theories.
     1.9 +
    1.10  
    1.11  *** HOLCF ***
    1.12  
    1.13 @@ -605,7 +608,7 @@
    1.14  
    1.15  *** ZF ***
    1.16  
    1.17 -* ZF/Constructible: consistency proof for AC (Gödel's constructible
    1.18 +* ZF/Constructible: consistency proof for AC (Gdel's constructible
    1.19  universe, etc.);
    1.20  
    1.21  * Main ZF: virtually all theories converted to new-style format;
    1.22 @@ -722,7 +725,7 @@
    1.23  multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
    1.24  
    1.25  * Pure: proper integration with ``locales''; unlike the original
    1.26 -version by Florian Kammüller, Isar locales package high-level proof
    1.27 +version by Florian Kammller, Isar locales package high-level proof
    1.28  contexts rather than raw logical ones (e.g. we admit to include
    1.29  attributes everywhere); operations on locales include merge and
    1.30  rename; support for implicit arguments (``structures''); simultaneous
    1.31 @@ -931,7 +934,7 @@
    1.32  the "cases" method);
    1.33  
    1.34  * HOL/GroupTheory: group theory examples including Sylow's theorem (by
    1.35 -Florian Kammüller);
    1.36 +Florian Kammller);
    1.37  
    1.38  * HOL/IMP: updated and converted to new-style theory format; several
    1.39  parts turned into readable document, with proper Isar proof texts and