--- a/src/HOL/Unix/document/root.tex Tue Jul 16 18:46:04 2002 +0200
+++ b/src/HOL/Unix/document/root.tex Tue Jul 16 18:46:13 2002 +0200
@@ -206,7 +206,7 @@
over the structure of file-systems and possible system transitions.
Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} is particularly well-suited for this
kind of application. By the present development we also demonstrate that the
-Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2000:isar-ref} for
+Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2002:isar-ref} for
readable formal proofs is sufficiently flexible to cover non-trivial
verification tasks as well. So far this has been the classical domain of
``interactive'' theorem proving systems based on unstructured tactic