# HG changeset patch
# User wenzelm
# Date 1026837973 -7200
# Node ID 60bc63b1385779e66bef1b1022c0d18feb37d5c5
# Parent  ec17b9cac1fb34247566e5636be45da715b9c6ac
tuned;

diff -r ec17b9cac1fb -r 60bc63b13857 src/HOL/Unix/document/root.bib
--- a/src/HOL/Unix/document/root.bib	Tue Jul 16 18:46:04 2002 +0200
+++ b/src/HOL/Unix/document/root.bib	Tue Jul 16 18:46:13 2002 +0200
@@ -1,10 +1,11 @@
 
-@Unpublished{Bauer-et-al:2001:HOL-Library,
-  author = 	 {Gertrud Bauer and Tobias Nipkow and Lawrence C Paulson and
-                  Thomas M Rasmussen and Markus Wenzel},
+@Unpublished{Bauer-et-al:2002:HOL-Library,
+  author = 	 {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and
+                  Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
+                  Markus Wenzel},
   title = 	 {The Supplemental {Isabelle/HOL} Library},
   note = 	 {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
-  year =	 2001
+  year =	 2002
 }
 
 @PhdThesis{Naraschewski:2001,
@@ -50,10 +51,10 @@
   crossref =     {tphols99}}
 
 
-@Manual{Wenzel:2000:isar-ref,
+@Manual{Wenzel:2002:isar-ref,
   author        = {Markus Wenzel},
   title         = {The {Isabelle/Isar} Reference Manual},
-  year          = 2000,
+  year          = 2002,
   institution   = {TU Munich},
   note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
 }
diff -r ec17b9cac1fb -r 60bc63b13857 src/HOL/Unix/document/root.tex
--- 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