--- a/src/Doc/manual.bib Mon Nov 25 14:50:31 2013 +0000
+++ b/src/Doc/manual.bib Mon Nov 25 16:00:09 2013 +0000
@@ -194,7 +194,7 @@
@incollection{basin91,
author = {David Basin and Matt Kaufmann},
title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
- Comparison},
+ Comparison},
crossref = {huet-plotkin91},
pages = {89-119}}
@@ -472,7 +472,7 @@
@book{constable86,
author = {R. L. Constable and others},
title = {Implementing Mathematics with the Nuprl Proof
- Development System},
+ Development System},
publisher = Prentice,
year = 1986}
@@ -505,7 +505,7 @@
@incollection{dybjer91,
author = {Peter Dybjer},
title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
- Theory and Their Set-Theoretic Semantics},
+ Theory and Their Set-Theoretic Semantics},
crossref = {huet-plotkin91},
pages = {280-306}}
@@ -533,7 +533,7 @@
@InProceedings{felty91a,
Author = {Amy Felty},
Title = {A Logic Program for Transforming Sequent Proofs to Natural
- Deduction Proofs},
+ Deduction Proofs},
crossref = {extensions91},
pages = {157-178}}
@@ -566,9 +566,9 @@
@inproceedings{OBJ,
author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
- and J. Meseguer},
+ and J. Meseguer},
title = {Principles of {OBJ2}},
- booktitle = POPL,
+ booktitle = POPL,
year = 1985,
pages = {52-66}}
@@ -576,7 +576,7 @@
@book{gallier86,
author = {J. H. Gallier},
- title = {Logic for Computer Science:
+ title = {Logic for Computer Science:
Foundations of Automatic Theorem Proving},
year = 1986,
publisher = {Harper \& Row}}
@@ -605,8 +605,8 @@
author = {Jean-Yves Girard},
title = {Proofs and Types},
year = 1989,
- publisher = CUP,
- note = {Translated by Yves LaFont and Paul Taylor}}
+ publisher = CUP,
+ note = {Translated by Yves Lafont and Paul Taylor}}
@Book{mgordon-hol,
editor = {M. J. C. Gordon and T. F. Melham},
@@ -777,21 +777,21 @@
@article{huet78,
author = {G. P. Huet and B. Lang},
- title = {Proving and Applying Program Transformations Expressed with
+ title = {Proving and Applying Program Transformations Expressed with
Second-Order Patterns},
journal = acta,
volume = 11,
- year = 1978,
+ year = 1978,
pages = {31-55}}
@inproceedings{huet88,
author = {G{\'e}rard Huet},
title = {Induction Principles Formalized in the {Calculus of
- Constructions}},
+ Constructions}},
booktitle = {Programming of Future Generation Computers},
editor = {K. Fuchi and M. Nivat},
year = 1988,
- pages = {205-216},
+ pages = {205-216},
publisher = {Elsevier}}
@inproceedings{Huffman-Kuncar:2013:lifting_transfer,
@@ -843,7 +843,7 @@
%K
@InProceedings{kammueller-locales,
- author = {Florian Kamm{\"u}ller and Markus Wenzel and
+ author = {Florian Kamm{\"u}ller and Markus Wenzel and
Lawrence C. Paulson},
title = {Locales: A Sectioning Concept for {Isabelle}},
crossref = {tphols99}}
@@ -944,7 +944,7 @@
author = {Gavin Lowe},
title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
Protocol using {CSP} and {FDR}},
- booktitle = {Tools and Algorithms for the Construction and Analysis
+ booktitle = {Tools and Algorithms for the Construction and Analysis
of Systems: second international workshop, TACAS '96},
editor = {T. Margaria and B. Steffen},
series = {LNCS 1055},
@@ -978,7 +978,7 @@
@incollection{melham89,
author = {Thomas F. Melham},
title = {Automating Recursive Type Definitions in Higher Order
- Logic},
+ Logic},
pages = {341-386},
crossref = {birtwistle89}}
@@ -1057,7 +1057,7 @@
@InProceedings{NaraschewskiW-TPHOLs98,
author = {Wolfgang Naraschewski and Markus Wenzel},
- title =
+ title =
{Object-Oriented Verification based on Record Subtyping in
Higher-Order Logic},
crossref = {tphols98}}
@@ -1190,8 +1190,8 @@
@book{nordstrom90,
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},
+ Introduction},
+ publisher = {Oxford University Press},
year = 1990}
%O
@@ -1251,7 +1251,7 @@
@InProceedings{paulson-COLOG,
author = {Lawrence C. Paulson},
title = {A Formulation of the Simple Theory of Types (for
- {Isabelle})},
+ {Isabelle})},
pages = {246-274},
crossref = {colog88},
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
@@ -1304,7 +1304,7 @@
%replaces paulson-final
@Article{paulson-mscs,
author = {Lawrence C. Paulson},
- title = {Final Coalgebras as Greatest Fixed Points
+ title = {Final Coalgebras as Greatest Fixed Points
in {ZF} Set Theory},
journal = {Mathematical Structures in Computer Science},
year = 1999,
@@ -1337,9 +1337,9 @@
crossref = {milner-fest}}
@book{milner-fest,
- title = {Proof, Language, and Interaction:
+ title = {Proof, Language, and Interaction:
Essays in Honor of {Robin Milner}},
- booktitle = {Proof, Language, and Interaction:
+ booktitle = {Proof, Language, and Interaction:
Essays in Honor of {Robin Milner}},
publisher = MIT,
year = 2000,
@@ -1427,7 +1427,7 @@
@book{paulson87,
author = {Lawrence C. Paulson},
title = {Logic and Computation: Interactive proof with Cambridge
- LCF},
+ LCF},
year = 1987,
publisher = CUP}
@@ -1470,7 +1470,7 @@
@article{pelletier86,
author = {F. J. Pelletier},
title = {Seventy-five Problems for Testing Automatic Theorem
- Provers},
+ Provers},
journal = JAR,
volume = 2,
pages = {191-216},
@@ -1486,13 +1486,13 @@
publisher = CUP,
year = 1993}
-@Article{pitts94,
+@Article{pitts94,
author = {Andrew M. Pitts},
title = {A Co-induction Principle for Recursively Defined Domains},
journal = TCS,
- volume = 124,
+ volume = 124,
pages = {195-219},
- year = 1994}
+ year = 1994}
@Article{plaisted90,
author = {David A. Plaisted},
@@ -1561,7 +1561,7 @@
@inproceedings{saaltink-fme,
author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
Dan Craigen and Irwin Meisels},
- title = {An {EVES} Data Abstraction Example},
+ title = {An {EVES} Data Abstraction Example},
pages = {578-596},
crossref = {fme93}}
@@ -1897,7 +1897,7 @@
author = {A. N. Whitehead and B. Russell},
title = {Principia Mathematica},
year = 1962,
- publisher = CUP,
+ publisher = CUP,
note = {Paperback edition to *56,
abridged from the 2nd edition (1927)}}
@@ -1982,9 +1982,9 @@
@book{birtwistle89,
editor = {Graham Birtwistle and P. A. Subrahmanyam},
title = {Current Trends in Hardware Verification and Automated
- Theorem Proving},
+ Theorem Proving},
booktitle = {Current Trends in Hardware Verification and Automated
- Theorem Proving},
+ Theorem Proving},
publisher = {Springer},
year = 1989}
@@ -1997,9 +1997,9 @@
@Proceedings{cade12,
editor = {Alan Bundy},
- title = {Automated Deduction --- {CADE}-12
+ title = {Automated Deduction --- {CADE}-12
International Conference},
- booktitle = {Automated Deduction --- {CADE}-12
+ booktitle = {Automated Deduction --- {CADE}-12
International Conference},
year = 1994,
series = {LNAI 814},
@@ -2059,7 +2059,7 @@
title = {Extensions of Logic Programming},
booktitle = {Extensions of Logic Programming},
year = 1991,
- series = {LNAI 475},
+ series = {LNAI 475},
publisher = {Springer}}
@proceedings{cade10,
@@ -2078,9 +2078,9 @@
year = 1993}
@book{wos-fest,
- title = {Automated Reasoning and its Applications:
+ title = {Automated Reasoning and its Applications:
Essays in Honor of {Larry Wos}},
- booktitle = {Automated Reasoning and its Applications:
+ booktitle = {Automated Reasoning and its Applications:
Essays in Honor of {Larry Wos}},
publisher = MIT,
year = 1997,