--- a/NEWS Thu Oct 05 14:04:56 2000 +0200
+++ b/NEWS Fri Oct 06 01:04:56 2000 +0200
@@ -243,10 +243,17 @@
* HOL/Algebra: new theory of rings and univariate polynomials, by
Clemens Ballarin;
-* HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese
+* HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese
Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M
Rasmussen;
+* HOL/Lattice: fundamental concepts of lattice theory and order
+structures, including duals, properties of bounds versus algebraic
+laws, lattice operations versus set-theoretic ones, the Knaster-Tarski
+Theorem for complete lattices etc.; may also serve as a demonstration
+for abstract algebraic reasoning using axiomatic type classes, and
+mathematics-style proof in Isabelle/Isar; by Markus Wenzel;
+
* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
von Oheimb;