# HG changeset patch
# User wenzelm
# Date 927884527 -7200
# Node ID 74e8f703f5f2318585148012632f0516862c185a
# Parent  9727e83f0578ee6e60a141888eeec8502c0f5944
tuned manual.bib;

diff -r 9727e83f0578 -r 74e8f703f5f2 doc-src/Inductive/ind-defs.tex
--- 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
diff -r 9727e83f0578 -r 74e8f703f5f2 doc-src/ZF/ZF.tex
--- 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.
 
diff -r 9727e83f0578 -r 74e8f703f5f2 doc-src/manual.bib
--- 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}