doc-src/manual.bib

   note =	 {\url{http://www.proofgeneral.org}}
 }
 
 %B
 
+@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
+title="Term Rewriting and All That",publisher=CUP,year=1998}
+
 @incollection{basin91,
   author	= {David Basin and Matt Kaufmann},
   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
 		   Comparison}, 
   crossref	= {huet-plotkin91},

   year		= 1977,
   publisher	= {Oxford University Press}}
 
 @incollection{dybjer91,
   author	= {Peter Dybjer},
-  title		= {Inductive Sets and Families in {Martin-L\"of's} Type
+  title		= {Inductive Sets and Families in {Martin-L{\"o}f's} Type
 		  Theory and Their Set-Theoretic Semantics}, 
   crossref	= {huet-plotkin91},
   pages		= {280-306}}
 
 @Article{dyckhoff,

   volume	= 11,
   year		= 1978, 
   pages		= {31-55}}
 
 @inproceedings{huet88,
-  author	= {G\'erard Huet},
+  author	= {G{\'e}rard Huet},
   title		= {Induction Principles Formalized in the {Calculus of
 		 Constructions}}, 
   booktitle	= {Programming of Future Generation Computers},
   editor	= {K. Fuchi and M. Nivat},
   year		= 1988,
   pages		= {205-216}, 
   publisher	= {Elsevier}}
+
+@Book{Huth-Ryan-book,
+  author	= {Michael Huth and Mark Ryan},
+  title		= {Logic in Computer Science. Modelling and reasoning about systems},
+  publisher	= CUP,
+  year		= 2000}
 
 @InProceedings{Harrison:1996:MizarHOL,
   author = 	 {J. Harrison},
   title = 	 {A {Mizar} Mode for {HOL}},
   pages =	 {203--220},

   title		= {Ordered Rewriting and Confluence},
   crossref	= {cade10},
   pages		= {366-380}}
 
 @book{martinlof84,
-  author	= {Per Martin-L\"of},
+  author	= {Per Martin-L{\"o}f},
   title		= {Intuitionistic type theory},
   year		= 1984,
   publisher	= {Bibliopolis}}
 
 @incollection{melham89,

   school	= {University of Edinburgh},
   year		= 1984}
 
 @article{MuellerNvOS99,
 author=
-{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
+{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
 
 @Manual{Muzalewski:Mizar,
   title = 	 {An Outline of {PC} {Mizar}},
   author =	 {Micha{\l} Muzalewski},

 
 @inproceedings{nipkow-W,
   author	= {Wolfgang Naraschewski and Tobias Nipkow},
   title		= {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
   booktitle	= {Types for Proofs and Programs: Intl. Workshop TYPES '96},
-  editor	= {E. Gim\'enez and C. Paulin-Mohring},
+  editor	= {E. Gim{\'e}nez and C. Paulin-Mohring},
   publisher	= Springer,
   series	= LNCS,
   volume	= 1512,
   pages		= {317-332},
   year		= 1998}

   year		= 1998}
 
 @manual{isabelle-HOL,
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   title		= {{Isabelle}'s Logics: {HOL}},
-  institution	= {Institut f\"ur Informatik, Technische Universi\"at
-                  M\"unchen and Computer Laboratory, University of Cambridge},
+  institution	= {Institut f{\"u}r Informatik, Technische Universi{\"a}t
+                  M{\"u}nchen and Computer Laboratory, University of Cambridge},
   note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
 
 @article{nipkow-prehofer,
   author	= {Tobias Nipkow and Christian Prehofer},
   title		= {Type Reconstruction for Type Classes},

   number	= 1,
   pages		= {15-58},
   year		= 1993}
 
 @book{nordstrom90,
-  author	= {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},
-  title		= {Programming in {Martin-L\"of}'s Type Theory.  An
+  author	= {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
+  title		= {Programming in {Martin-L{\"o}f}'s Type Theory.  An
 		 Introduction}, 
   publisher	= {Oxford University Press}, 
   year		= 1990}
 
 %O

 }
 
 %V
 
 @Unpublished{voelker94,
-  author	= {Norbert V\"olker},
+  author	= {Norbert V{\"o}lker},
   title		= {The Verification of a Timer Program using {Isabelle/HOL}},
   url		= {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
   year		= 1994,
   month		= aug}
 

   year		= 1994,
   series	= {LNAI 814},
   publisher	= {Springer}}
 
 @book{types94,
-  editor	= {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
+  editor	= {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith},
   title		= TYPES # {: International Workshop {TYPES '94}},
   booktitle	= TYPES # {: International Workshop {TYPES '94}},
   year		= 1995,
   publisher	= {Springer},
   series	= {LNCS 996}}
 
 @book{huet-plotkin91,
-  editor	= {{G\'erard} Huet and Gordon Plotkin},
+  editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
   title		= {Logical Frameworks},
   booktitle	= {Logical Frameworks},
   publisher	= CUP,
   year		= 1991}
 
 @book{huet-plotkin93,
-  editor	= {{G\'erard} Huet and Gordon Plotkin},
+  editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
   title		= {Logical Environments},
   booktitle	= {Logical Environments},
   publisher	= CUP,
   year		= 1993}
 

   year		= {Published 1994},
   publisher	= {Springer},
   series	= {LNCS 780}}
 
 @proceedings{colog88,
-  editor	= {P. Martin-L\"of and G. Mints},
+  editor	= {P. Martin-L{\"o}f and G. Mints},
   title		= {COLOG-88: International Conference on Computer Logic},
   booktitle	= {COLOG-88: International Conference on Computer Logic},
   year		= {Published 1990},
   publisher	= {Springer},
   organization	= {Estonian Academy of Sciences},