1.1 --- a/doc-src/Inductive/ind-defs.tex	Thu May 27 20:49:10 1999 +0200
     1.2 +++ b/doc-src/Inductive/ind-defs.tex	Fri May 28 11:42:07 1999 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4  \end{eqnarray*}   
     1.5  These equations are instances of the Knaster-Tarski theorem, which states
     1.6  that every monotonic function over a complete lattice has a
     1.7 -fixedpoint~\cite{davey&priestley}.  It is obvious from their definitions
     1.8 +fixedpoint~\cite{davey-priestley}.  It is obvious from their definitions
     1.9  that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
    1.10  
    1.11  This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to

     2.1 --- a/doc-src/ZF/ZF.tex	Thu May 27 20:49:10 1999 +0200
     2.2 +++ b/doc-src/ZF/ZF.tex	Fri May 28 11:42:07 1999 +0200
     2.3 @@ -1173,7 +1173,7 @@
     2.4  These are essential to many definitions that follow, including the natural
     2.5  numbers and the transitive closure operator.  The (co)inductive definition
     2.6  package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
     2.7 -Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
     2.8 +Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski
     2.9  Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
    2.10  proofs.
    2.11  

     3.1 --- a/doc-src/manual.bib	Thu May 27 20:49:10 1999 +0200
     3.2 +++ b/doc-src/manual.bib	Fri May 28 11:42:07 1999 +0200
     3.3 @@ -176,7 +176,7 @@
     3.4  
     3.5  %D
     3.6  
     3.7 -@Book{davey&priestley,
     3.8 +@Book{davey-priestley,
     3.9    author	= {B. A. Davey and H. A. Priestley},
    3.10    title		= {Introduction to Lattices and Order},
    3.11    publisher	= CUP,
    3.12 @@ -461,7 +461,7 @@
    3.13  
    3.14  @article{MuellerNvOS99,
    3.15  author=
    3.16 -{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch},
    3.17 +{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
    3.18  title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
    3.19  
    3.20  %N
    3.21 @@ -511,7 +511,7 @@
    3.22    author	= {Tobias Nipkow},
    3.23    pages		= {64-74},
    3.24    crossref	= {lics8},
    3.25 -  url		= {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
    3.26 +  url		= {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}},
    3.27    keywords	= {unification}}
    3.28  
    3.29  @article{nipkow-IMP,
    3.30 @@ -560,7 +560,7 @@
    3.31    author	= {S. Owre and N. Shankar and J. M. Rushby},
    3.32    organization	= {Computer Science Laboratory, SRI International},
    3.33    address	= {Menlo Park, CA},
    3.34 -  note		= {Beta release},
    3.35 +  note          = {Beta release},
    3.36    year		= 1993,
    3.37    month		= apr,
    3.38    url		= {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
    3.39 @@ -697,7 +697,7 @@
    3.40    number	= 3,
    3.41    pages		= {353-389},
    3.42    year		= 1993,
    3.43 -  url		= {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
    3.44 +  url		= {\url{ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}}
    3.45  
    3.46  @Article{paulson-set-II,
    3.47    author	= {Lawrence C. Paulson},
    3.48 @@ -853,7 +853,7 @@
    3.49  @Unpublished{voelker94,
    3.50    author	= {Norbert V\"olker},
    3.51    title		= {The Verification of a Timer Program using {Isabelle/HOL}},
    3.52 -  url		= {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},
    3.53 +  url		= {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
    3.54    year		= 1994,
    3.55    month		= aug}
    3.56