1.1 --- a/doc-src/manual.bib Wed Oct 11 00:03:22 2000 +0200
1.2 +++ b/doc-src/manual.bib Wed Oct 11 09:09:06 2000 +0200
1.3 @@ -109,6 +109,9 @@
1.4
1.5 %B
1.6
1.7 +@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
1.8 +title="Term Rewriting and All That",publisher=CUP,year=1998}
1.9 +
1.10 @incollection{basin91,
1.11 author = {David Basin and Matt Kaufmann},
1.12 title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
1.13 @@ -231,7 +234,7 @@
1.14
1.15 @incollection{dybjer91,
1.16 author = {Peter Dybjer},
1.17 - title = {Inductive Sets and Families in {Martin-L\"of's} Type
1.18 + title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
1.19 Theory and Their Set-Theoretic Semantics},
1.20 crossref = {huet-plotkin91},
1.21 pages = {280-306}}
1.22 @@ -400,7 +403,7 @@
1.23 pages = {31-55}}
1.24
1.25 @inproceedings{huet88,
1.26 - author = {G\'erard Huet},
1.27 + author = {G{\'e}rard Huet},
1.28 title = {Induction Principles Formalized in the {Calculus of
1.29 Constructions}},
1.30 booktitle = {Programming of Future Generation Computers},
1.31 @@ -409,6 +412,12 @@
1.32 pages = {205-216},
1.33 publisher = {Elsevier}}
1.34
1.35 +@Book{Huth-Ryan-book,
1.36 + author = {Michael Huth and Mark Ryan},
1.37 + title = {Logic in Computer Science. Modelling and reasoning about systems},
1.38 + publisher = CUP,
1.39 + year = 2000}
1.40 +
1.41 @InProceedings{Harrison:1996:MizarHOL,
1.42 author = {J. Harrison},
1.43 title = {A {Mizar} Mode for {HOL}},
1.44 @@ -462,7 +471,7 @@
1.45 pages = {366-380}}
1.46
1.47 @book{martinlof84,
1.48 - author = {Per Martin-L\"of},
1.49 + author = {Per Martin-L{\"o}f},
1.50 title = {Intuitionistic type theory},
1.51 year = 1984,
1.52 publisher = {Bibliopolis}}
1.53 @@ -520,7 +529,7 @@
1.54
1.55 @article{MuellerNvOS99,
1.56 author=
1.57 -{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
1.58 +{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
1.59 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
1.60
1.61 @Manual{Muzalewski:Mizar,
1.62 @@ -552,7 +561,7 @@
1.63 author = {Wolfgang Naraschewski and Tobias Nipkow},
1.64 title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
1.65 booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},
1.66 - editor = {E. Gim\'enez and C. Paulin-Mohring},
1.67 + editor = {E. Gim{\'e}nez and C. Paulin-Mohring},
1.68 publisher = Springer,
1.69 series = LNCS,
1.70 volume = 1512,
1.71 @@ -607,8 +616,8 @@
1.72 @manual{isabelle-HOL,
1.73 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
1.74 title = {{Isabelle}'s Logics: {HOL}},
1.75 - institution = {Institut f\"ur Informatik, Technische Universi\"at
1.76 - M\"unchen and Computer Laboratory, University of Cambridge},
1.77 + institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
1.78 + M{\"u}nchen and Computer Laboratory, University of Cambridge},
1.79 note = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
1.80
1.81 @article{nipkow-prehofer,
1.82 @@ -630,8 +639,8 @@
1.83 year = 1993}
1.84
1.85 @book{nordstrom90,
1.86 - author = {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},
1.87 - title = {Programming in {Martin-L\"of}'s Type Theory. An
1.88 + author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
1.89 + title = {Programming in {Martin-L{\"o}f}'s Type Theory. An
1.90 Introduction},
1.91 publisher = {Oxford University Press},
1.92 year = 1990}
1.93 @@ -974,7 +983,7 @@
1.94 %V
1.95
1.96 @Unpublished{voelker94,
1.97 - author = {Norbert V\"olker},
1.98 + author = {Norbert V{\"o}lker},
1.99 title = {The Verification of a Timer Program using {Isabelle/HOL}},
1.100 url = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
1.101 year = 1994,
1.102 @@ -1123,7 +1132,7 @@
1.103 publisher = {Springer}}
1.104
1.105 @book{types94,
1.106 - editor = {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
1.107 + editor = {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith},
1.108 title = TYPES # {: International Workshop {TYPES '94}},
1.109 booktitle = TYPES # {: International Workshop {TYPES '94}},
1.110 year = 1995,
1.111 @@ -1131,14 +1140,14 @@
1.112 series = {LNCS 996}}
1.113
1.114 @book{huet-plotkin91,
1.115 - editor = {{G\'erard} Huet and Gordon Plotkin},
1.116 + editor = {{G{\'e}rard} Huet and Gordon Plotkin},
1.117 title = {Logical Frameworks},
1.118 booktitle = {Logical Frameworks},
1.119 publisher = CUP,
1.120 year = 1991}
1.121
1.122 @book{huet-plotkin93,
1.123 - editor = {{G\'erard} Huet and Gordon Plotkin},
1.124 + editor = {{G{\'e}rard} Huet and Gordon Plotkin},
1.125 title = {Logical Environments},
1.126 booktitle = {Logical Environments},
1.127 publisher = CUP,
1.128 @@ -1155,7 +1164,7 @@
1.129 series = {LNCS 780}}
1.130
1.131 @proceedings{colog88,
1.132 - editor = {P. Martin-L\"of and G. Mints},
1.133 + editor = {P. Martin-L{\"o}f and G. Mints},
1.134 title = {COLOG-88: International Conference on Computer Logic},
1.135 booktitle = {COLOG-88: International Conference on Computer Logic},
1.136 year = {Published 1990},