--- a/doc-src/Inductive/ind-defs.tex Thu May 27 20:49:10 1999 +0200
+++ b/doc-src/Inductive/ind-defs.tex Fri May 28 11:42:07 1999 +0200
@@ -219,7 +219,7 @@
\end{eqnarray*}
These equations are instances of the Knaster-Tarski theorem, which states
that every monotonic function over a complete lattice has a
-fixedpoint~\cite{davey&priestley}. It is obvious from their definitions
+fixedpoint~\cite{davey-priestley}. It is obvious from their definitions
that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to
--- a/doc-src/ZF/ZF.tex Thu May 27 20:49:10 1999 +0200
+++ b/doc-src/ZF/ZF.tex Fri May 28 11:42:07 1999 +0200
@@ -1173,7 +1173,7 @@
These are essential to many definitions that follow, including the natural
numbers and the transitive closure operator. The (co)inductive definition
package also uses the fixedpoint operators~\cite{paulson-CADE}. See
-Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
+Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski
Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
proofs.
--- a/doc-src/manual.bib Thu May 27 20:49:10 1999 +0200
+++ b/doc-src/manual.bib Fri May 28 11:42:07 1999 +0200
@@ -176,7 +176,7 @@
%D
-@Book{davey&priestley,
+@Book{davey-priestley,
author = {B. A. Davey and H. A. Priestley},
title = {Introduction to Lattices and Order},
publisher = CUP,
@@ -461,7 +461,7 @@
@article{MuellerNvOS99,
author=
-{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch},
+{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
%N
@@ -511,7 +511,7 @@
author = {Tobias Nipkow},
pages = {64-74},
crossref = {lics8},
- url = {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
+ url = {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}},
keywords = {unification}}
@article{nipkow-IMP,
@@ -560,7 +560,7 @@
author = {S. Owre and N. Shankar and J. M. Rushby},
organization = {Computer Science Laboratory, SRI International},
address = {Menlo Park, CA},
- note = {Beta release},
+ note = {Beta release},
year = 1993,
month = apr,
url = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
@@ -697,7 +697,7 @@
number = 3,
pages = {353-389},
year = 1993,
- url = {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
+ url = {\url{ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}}
@Article{paulson-set-II,
author = {Lawrence C. Paulson},
@@ -853,7 +853,7 @@
@Unpublished{voelker94,
author = {Norbert V\"olker},
title = {The Verification of a Timer Program using {Isabelle/HOL}},
- url = {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},
+ url = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
year = 1994,
month = aug}