--- a/doc-src/manual.bib Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/manual.bib Wed Oct 11 09:09:06 2000 +0200
@@ -109,6 +109,9 @@
%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
@@ -231,7 +234,7 @@
@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}}
@@ -400,7 +403,7 @@
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},
@@ -409,6 +412,12 @@
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}},
@@ -462,7 +471,7 @@
pages = {366-380}}
@book{martinlof84,
- author = {Per Martin-L\"of},
+ author = {Per Martin-L{\"o}f},
title = {Intuitionistic type theory},
year = 1984,
publisher = {Bibliopolis}}
@@ -520,7 +529,7 @@
@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,
@@ -552,7 +561,7 @@
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,
@@ -607,8 +616,8 @@
@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,
@@ -630,8 +639,8 @@
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}
@@ -974,7 +983,7 @@
%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,
@@ -1123,7 +1132,7 @@
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,
@@ -1131,14 +1140,14 @@
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,
@@ -1155,7 +1164,7 @@
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},