--- 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}}
}
--- 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