diff -r cd89ce2795ab -r 8f2c27041a8e NEWS
--- 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;