--- a/NEWS Tue Jan 23 15:48:35 2001 +0100
+++ b/NEWS Tue Jan 23 18:05:53 2001 +0100
@@ -102,6 +102,10 @@
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
(as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
+* HOL/Unix: "Some aspects of Unix file-system security", a typical
+modelling and verification task performed in Isabelle/HOL +
+Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).
+
* HOL basics: added overloaded operations "inverse" and "divide"
(infix "/"), syntax for generic "abs" operation, generic summation
operator;