diff -r 6a753a6d6738 -r c120262044b6 doc-src/manual.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/manual.bib	Wed May 05 16:44:42 1999 +0200
@@ -0,0 +1,937 @@
+% BibTeX database for the Isabelle documentation
+%
+% Lawrence C Paulson $Id$
+
+%publishers
+@string{AP="Academic Press"}
+@string{CUP="Cambridge University Press"}
+@string{IEEE="{\sc ieee} Computer Society Press"}
+@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
+@string{MIT="MIT Press"}
+@string{NH="North-Holland"}
+@string{Prentice="Prentice-Hall"}
+@string{Springer="Springer-Verlag"}
+
+%institutions
+@string{CUCL="Computer Laboratory, University of Cambridge"}
+
+%journals
+@string{FAC="Formal Aspects Comput."}
+@string{JAR="J. Auto. Reas."}
+@string{JCS="J. Comput. Secur."}
+@string{JFP="J. Func. Prog."}
+@string{JLC="J. Logic and Comput."}
+@string{JLP="J. Logic Prog."}
+@string{JSC="J. Symb. Comput."}
+@string{JSL="J. Symb. Logic"}
+@string{SIGPLAN="{SIGPLAN} Notices"}
+
+%conferences
+@string{CADE="International Conference on Automated Deduction"}
+@string{POPL="Symposium on Principles of Programming Languages"}
+@string{TYPES="Types for Proofs and Programs"}
+
+
+%A
+
+@incollection{abramsky90,
+  author	= {Samson Abramsky},
+  title		= {The Lazy Lambda Calculus},
+  pages		= {65-116},
+  editor	= {David A. Turner},
+  booktitle	= {Research Topics in Functional Programming},
+  publisher	= {Addison-Wesley},
+  year		= 1990}
+
+@Unpublished{abrial93,
+  author	= {J. R. Abrial and G. Laffitte},
+  title		= {Towards the Mechanization of the Proofs of some Classical
+		  Theorems of Set Theory},
+  note		= {preprint},
+  year		= 1993,
+  month		= Feb}
+
+@incollection{aczel77,
+  author	= {Peter Aczel},
+  title		= {An Introduction to Inductive Definitions},
+  pages		= {739-782},
+  crossref	= {barwise-handbk}}
+
+@Book{aczel88,
+  author	= {Peter Aczel},
+  title		= {Non-Well-Founded Sets},
+  publisher	= {CSLI},
+  year		= 1988}
+
+@InProceedings{alf,
+  author	= {Lena Magnusson and Bengt {Nordstr\"{o}m}},
+  title		= {The {ALF} Proof Editor and Its Proof Engine},
+  crossref	= {types93},
+  pages		= {213-237}}
+
+@book{andrews86,
+  author	= "Peter Andrews",
+  title		= "An Introduction to Mathematical Logic and Type Theory: to Truth
+through Proof",
+  publisher	= AP,
+  series	= "Computer Science and Applied Mathematics",
+  year		= 1986}
+
+%B
+
+@incollection{basin91,
+  author	= {David Basin and Matt Kaufmann},
+  title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
+		   Comparison}, 
+  crossref	= {huet-plotkin91},
+  pages		= {89-119}}
+
+@Article{boyer86,
+  author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
+		   Overbeek and Mark Stickel and Lawrence Wos},
+  title		= {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
+		   Axioms},
+  journal	= JAR,
+  year		= 1986,
+  volume	= 2,
+  number	= 3,
+  pages		= {287-327}}
+
+@book{bm79,
+  author	= {Robert S. Boyer and J Strother Moore},
+  title		= {A Computational Logic},
+  publisher	= {Academic Press},
+  year		= 1979}
+
+@book{bm88book,
+  author	= {Robert S. Boyer and J Strother Moore},
+  title		= {A Computational Logic Handbook},
+  publisher	= {Academic Press},
+  year		= 1988}
+
+@Article{debruijn72,
+  author	= {N. G. de Bruijn},
+  title		= {Lambda Calculus Notation with Nameless Dummies,
+	a Tool for Automatic Formula Manipulation,
+	with Application to the {Church-Rosser Theorem}},
+  journal	= {Indag. Math.},
+  volume	= 34,
+  pages		= {381-392},
+  year		= 1972}
+
+%C
+
+@TechReport{camilleri92,
+  author	= {J. Camilleri and T. F. Melham},
+  title		= {Reasoning with Inductively Defined Relations in the
+		 {HOL} Theorem Prover},
+  institution	= CUCL,
+  year		= 1992,
+  number	= 265,
+  month		= Aug}
+
+@Book{charniak80,
+  author	= {E. Charniak and C. K. Riesbeck and D. V. McDermott},
+  title		= {Artificial Intelligence Programming},
+  publisher	= {Lawrence Erlbaum Associates},
+  year		= 1980}
+
+@article{church40,
+  author	= "Alonzo Church",
+  title		= "A Formulation of the Simple Theory of Types",
+  journal	= JSL,
+  year		= 1940,
+  volume	= 5,
+  pages		= "56-68"}
+
+@PhdThesis{coen92,
+  author	= {Martin D. Coen},
+  title		= {Interactive Program Derivation},
+  school	= {University of Cambridge},
+  note		= {Computer Laboratory Technical Report 272},
+  month		= nov,
+  year		= 1992}
+
+@book{constable86,
+  author	= {R. L. Constable and others},
+  title		= {Implementing Mathematics with the Nuprl Proof
+		 Development System}, 
+  publisher	= Prentice,
+  year		= 1986}
+
+%D
+
+@Book{davey&priestley,
+  author	= {B. A. Davey and H. A. Priestley},
+  title		= {Introduction to Lattices and Order},
+  publisher	= CUP,
+  year		= 1990}
+
+@Book{devlin79,
+  author	= {Keith J. Devlin},
+  title		= {Fundamentals of Contemporary Set Theory},
+  publisher	= {Springer},
+  year		= 1979}
+
+@book{dummett,
+  author	= {Michael Dummett},
+  title		= {Elements of Intuitionism},
+  year		= 1977,
+  publisher	= {Oxford University Press}}
+
+@incollection{dybjer91,
+  author	= {Peter Dybjer},
+  title		= {Inductive Sets and Families in {Martin-L\"of's} Type
+		  Theory and Their Set-Theoretic Semantics}, 
+  crossref	= {huet-plotkin91},
+  pages		= {280-306}}
+
+@Article{dyckhoff,
+  author	= {Roy Dyckhoff},
+  title		= {Contraction-Free Sequent Calculi for Intuitionistic Logic},
+  journal	= JSL,
+  year		= 1992,
+  volume	= 57,
+  number	= 3,
+  pages		= {795-807}}
+
+%F
+
+@InProceedings{felty91a,
+  Author	= {Amy Felty},
+  Title		= {A Logic Program for Transforming Sequent Proofs to Natural
+		  Deduction Proofs}, 
+  crossref	= {extensions91},
+  pages		= {157-178}}
+
+@TechReport{frost93,
+  author	= {Jacob Frost},
+  title		= {A Case Study of Co-induction in {Isabelle HOL}},
+  institution	= CUCL,
+  number	= 308,
+  year		= 1993,
+  month		= Aug}
+
+%revised version of frost93
+@TechReport{frost95,
+  author	= {Jacob Frost},
+  title		= {A Case Study of Co-induction in {Isabelle}},
+  institution	= CUCL,
+  number	= 359,
+  year		= 1995,
+  month		= Feb}
+
+@inproceedings{OBJ,
+  author	= {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
+		 and J. Meseguer}, 
+  title		= {Principles of {OBJ2}},
+  booktitle	= POPL, 
+  year		= 1985,
+  pages		= {52-66}}
+
+%G
+
+@book{gallier86,
+  author	= {J. H. Gallier},
+  title		= {Logic for Computer Science: 
+		Foundations of Automatic Theorem Proving},
+  year		= 1986,
+  publisher	= {Harper \& Row}}
+
+@Book{galton90,
+  author	= {Antony Galton},
+  title		= {Logic for Information Technology},
+  publisher	= {Wiley},
+  year		= 1990}
+
+@InProceedings{gimenez-codifying,
+  author	= {Eduardo Gim{\'e}nez},
+  title		= {Codifying Guarded Definitions with Recursive Schemes},
+  crossref	= {types94},
+  pages		= {39-59}
+}
+
+@Book{mgordon-hol,
+  author	= {M. J. C. Gordon and T. F. Melham},
+  title		= {Introduction to {HOL}: A Theorem Proving Environment for
+		 Higher Order Logic},
+  publisher	= CUP,
+  year		= 1993}
+
+@book{mgordon79,
+  author	= {Michael J. C. Gordon and Robin Milner and Christopher P.
+		 Wadsworth},
+  title		= {Edinburgh {LCF}: A Mechanised Logic of Computation},
+  year		= 1979,
+  publisher	= {Springer},
+  series	= {LNCS 78}}
+
+@InProceedings{gunter-trees,
+  author	= {Elsa L. Gunter},
+  title		= {A Broader Class of Trees for Recursive Type Definitions for
+		  {HOL}},
+  crossref	= {hug93},
+  pages		= {141-154}}
+
+%H
+
+@Book{halmos60,
+  author	= {Paul R. Halmos},
+  title		= {Naive Set Theory},
+  publisher	= {Van Nostrand},
+  year		= 1960}
+
+@Book{hennessy90,
+  author	= {Matthew Hennessy},
+  title		= {The Semantics of Programming Languages: An Elementary
+		  Introduction Using Structural Operational Semantics},
+  publisher	= {Wiley},
+  year		= 1990}
+
+@Article{haskell-report,
+  author	= {Paul Hudak and Simon Peyton Jones and Philip Wadler},
+  title		= {Report on the Programming Language {Haskell}: A
+		 Non-strict, Purely Functional Language},
+  journal	= SIGPLAN,
+  year		= 1992,
+  volume	= 27,
+  number	= 5,
+  month		= May,
+  note		= {Version 1.2}}
+
+@Article{haskell-tutorial,
+  author	= {Paul Hudak and Joseph H. Fasel},
+  title		= {A Gentle Introduction to {Haskell}},
+  journal	= SIGPLAN,
+  year		= 1992,
+  volume	= 27,
+  number	= 5,
+  month		= May}
+
+@article{huet75,
+  author	= {G. P. Huet},
+  title		= {A Unification Algorithm for Typed $\lambda$-Calculus},
+  journal	= TCS,
+  volume	= 1,
+  year		= 1975,
+  pages		= {27-57}}
+
+@article{huet78,
+  author	= {G. P. Huet and B. Lang},
+  title		= {Proving and Applying Program Transformations Expressed with 
+			Second-Order Patterns},
+  journal	= acta,
+  volume	= 11,
+  year		= 1978, 
+  pages		= {31-55}}
+
+@inproceedings{huet88,
+  author	= {G\'erard 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}}
+
+%K
+
+@Book{kunen80,
+  author	= {Kenneth Kunen},
+  title		= {Set Theory: An Introduction to Independence Proofs},
+  publisher	= NH,
+  year		= 1980}
+
+%M
+
+@Article{mw81,
+  author	= {Zohar Manna and Richard Waldinger},
+  title		= {Deductive Synthesis of the Unification Algorithm},
+  journal	= SCP,
+  year		= 1981,
+  volume	= 1,
+  number	= 1,
+  pages		= {5-48}}
+
+@InProceedings{martin-nipkow,
+  author	= {Ursula Martin and Tobias Nipkow},
+  title		= {Ordered Rewriting and Confluence},
+  crossref	= {cade10},
+  pages		= {366-380}}
+
+@book{martinlof84,
+  author	= {Per Martin-L\"of},
+  title		= {Intuitionistic type theory},
+  year		= 1984,
+  publisher	= {Bibliopolis}}
+
+@incollection{melham89,
+  author	= {Thomas F. Melham},
+  title		= {Automating Recursive Type Definitions in Higher Order
+		 Logic}, 
+  pages		= {341-386},
+  crossref	= {birtwistle89}}
+
+@Article{miller-mixed,
+  Author	= {Dale Miller},
+  Title		= {Unification Under a Mixed Prefix},
+  journal	= JSC,
+  volume	= 14,
+  number	= 4,
+  pages		= {321-358},
+  Year		= 1992}
+
+@Article{milner78,
+  author	= {Robin Milner},
+  title		= {A Theory of Type Polymorphism in Programming},
+  journal	= "J. Comp.\ Sys.\ Sci.",
+  year		= 1978,
+  volume	= 17,
+  pages		= {348-375}}
+
+@TechReport{milner-ind,
+  author	= {Robin Milner},
+  title		= {How to Derive Inductions in {LCF}},
+  institution	= Edinburgh,
+  year		= 1980,
+  type		= {note}}
+
+@Article{milner-coind,
+  author	= {Robin Milner and Mads Tofte},
+  title		= {Co-induction in Relational Semantics},
+  journal	= TCS,
+  year		= 1991,
+  volume	= 87,
+  pages		= {209-220}}
+
+@Book{milner89,
+  author	= {Robin Milner},
+  title		= {Communication and Concurrency},
+  publisher	= Prentice,
+  year		= 1989}
+
+@PhdThesis{monahan84,
+  author	= {Brian Q. Monahan},
+  title		= {Data Type Proofs using Edinburgh {LCF}},
+  school	= {University of Edinburgh},
+  year		= 1984}
+
+%N
+
+@InProceedings{NaraschewskiW-TPHOLs98,
+  author	= {Wolfgang Naraschewski and Markus Wenzel},
+  title		= 
+{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
+  booktitle	= {Theorem Proving in Higher Order Logics (TPHOLs'98)},
+  publisher	= Springer,
+  volume	= 1479,
+  series	= LNCS,
+  year		= 1998}
+
+@inproceedings{nazareth-nipkow,
+  author	= {Dieter Nazareth and Tobias Nipkow},
+  title		= {Formal Verification of Algorithm {W}: The Monomorphic Case},
+  crossref	= {tphols96},
+  pages		= {331-345},
+  year		= 1996}
+
+@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},
+  publisher	= Springer,
+  series	= LNCS,
+  volume	= 1512,
+  pages		= {317-332},
+  year		= 1998}
+
+@inproceedings{Nipkow-CR,
+  author	= {Tobias Nipkow},
+  title		= {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
+  booktitle	= {Automated Deduction --- CADE-13},
+  editor	= {M. McRobbie and J.K. Slaney},
+  publisher	= Springer,
+  series	= LNCS,
+  volume	= 1104,
+  pages		= {733-747},
+  year		= 1996}
+
+% WAS Nipkow-LICS-93
+@InProceedings{nipkow-patterns,
+  title		= {Functional Unification of Higher-Order Patterns},
+  author	= {Tobias Nipkow},
+  pages		= {64-74},
+  crossref	= {lics8},
+  url		= {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
+  keywords	= {unification}}
+
+@article{nipkow-IMP,
+  author	= {Tobias Nipkow},
+  title		= {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
+  journal	= FAC,
+  volume	= 10,
+  pages		= {171-186},
+  year		= 1998}
+
+@article{nipkow-prehofer,
+  author	= {Tobias Nipkow and Christian Prehofer},
+  title		= {Type Reconstruction for Type Classes},
+  journal	= JFP,
+  volume	= 5,
+  number	= 2,
+  year		= 1995,
+  pages		= {201-224}}
+
+@Article{noel,
+  author	= {Philippe No{\"e}l},
+  title		= {Experimenting with {Isabelle} in {ZF} Set Theory},
+  journal	= JAR,
+  volume	= 10,
+  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
+		 Introduction}, 
+  publisher	= {Oxford University Press}, 
+  year		= 1990}
+
+%O
+
+@Manual{pvs-language,
+  title		= {The {PVS} specification language},
+  author	= {S. Owre and N. Shankar and J. M. Rushby},
+  organization	= {Computer Science Laboratory, SRI International},
+  address	= {Menlo Park, CA},
+  note		= {Beta release},
+  year		= 1993,
+  month		= apr,
+  url		= {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}}
+
+%P
+
+% replaces paulin92
+@InProceedings{paulin-tlca,
+  author	= {Christine Paulin-Mohring},
+  title		= {Inductive Definitions in the System {Coq}: Rules and
+		 Properties},
+  crossref	= {tlca93},
+  pages		= {328-345}}
+
+@InProceedings{paulson-CADE,
+  author	= {Lawrence C. Paulson},
+  title		= {A Fixedpoint Approach to Implementing (Co)Inductive
+		  Definitions},
+  pages		= {148-161},
+  crossref	= {cade12}}
+
+@InProceedings{paulson-COLOG,
+  author	= {Lawrence C. Paulson},
+  title		= {A Formulation of the Simple Theory of Types (for
+		 {Isabelle})}, 
+  pages		= {246-274},
+  crossref	= {colog88},
+  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}
+
+@Article{paulson-coind,
+  author	= {Lawrence C. Paulson},
+  title		= {Mechanizing Coinduction and Corecursion in Higher-Order
+		  Logic},
+  journal	= JLC,
+  year		= 1997,
+  volume	= 7,
+  number	= 2,
+  month		= mar,
+  pages		= {175-204}}
+
+@techreport{isabelle-ZF,
+  author	= {Lawrence C. Paulson},
+  title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
+  institution	= CUCL,
+  year		= 1999}
+
+@article{paulson-found,
+  author	= {Lawrence C. Paulson},
+  title		= {The Foundation of a Generic Theorem Prover},
+  journal	= JAR,
+  volume	= 5,
+  number	= 3,
+  pages		= {363-397},
+  year		= 1989,
+  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}
+
+%replaces paulson-final
+@Article{paulson-mscs,
+  author	= {Lawrence C. Paulson},
+  title		= {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
+  journal	= {Mathematical Structures in Computer Science},
+  year		= 1999,
+  volume	= 9,
+  note		= {in press}}
+
+@InCollection{paulson-generic,
+  author	= {Lawrence C. Paulson},
+  title		= {Generic Automatic Proof Tools},
+  crossref	= {wos-fest},
+  chapter	= 3}
+
+@Article{paulson-gr,
+  author	= {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
+  title		= {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
+		  Choice},
+  journal	= JAR,
+  year		= 1996,
+  volume	= 17,
+  number	= 3,
+  month		= dec,
+  pages		= {291-323}}
+
+@InCollection{paulson-handbook,
+  author	= {Lawrence C. Paulson},
+  title		= {Designing a Theorem Prover},
+  crossref	= {handbk-lics2},
+  pages		= {415-475}}
+
+@Book{paulson-isa-book,
+  author	= {Lawrence C. Paulson},
+  title		= {Isabelle: A Generic Theorem Prover},
+  publisher	= {Springer},
+  year		= 1994,
+  note		= {LNCS 828}}
+
+@InCollection{paulson-markt,
+  author	= {Lawrence C. Paulson},
+  title		= {Tool Support for Logics of Programs},
+  booktitle	= {Mathematical Methods in Program Development:
+                  Summer School Marktoberdorf 1996},
+  publisher	= {Springer},
+  pages		= {461-498},
+  year		= {Published 1997},
+  editor	= {Manfred Broy},
+  series	= {NATO ASI Series F}}
+
+%replaces Paulson-ML and paulson91
+@book{paulson-ml2,
+  author	= {Lawrence C. Paulson},
+  title		= {{ML} for the Working Programmer},
+  year		= 1996,
+  edition	= {2nd},
+  publisher	= CUP}
+
+@article{paulson-natural,
+  author	= {Lawrence C. Paulson},
+  title		= {Natural Deduction as Higher-order Resolution},
+  journal	= JLP,
+  volume	= 3,
+  pages		= {237-258},
+  year		= 1986,
+  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}
+
+@Article{paulson-set-I,
+  author	= {Lawrence C. Paulson},
+  title		= {Set Theory for Verification: {I}.  {From}
+		 Foundations to Functions},
+  journal	= JAR,
+  volume	= 11,
+  number	= 3,
+  pages		= {353-389},
+  year		= 1993,
+  url		= {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
+
+@Article{paulson-set-II,
+  author	= {Lawrence C. Paulson},
+  title		= {Set Theory for Verification: {II}.  {Induction} and
+		 Recursion},
+  journal	= JAR,
+  volume	= 15,
+  number	= 2,
+  pages		= {167-215},
+  year		= 1995,
+  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}
+
+@article{paulson85,
+  author	= {Lawrence C. Paulson},
+  title		= {Verifying the Unification Algorithm in {LCF}},
+  journal	= SCP,
+  volume	= 5,
+  pages		= {143-170},
+  year		= 1985}
+
+%replqces Paulson-LCF
+@book{paulson87,
+  author	= {Lawrence C. Paulson},
+  title		= {Logic and Computation: Interactive proof with Cambridge
+		 LCF}, 
+  year		= 1987,
+  publisher	= CUP}
+
+@incollection{paulson700,
+  author	= {Lawrence C. Paulson},
+  title		= {{Isabelle}: The Next 700 Theorem Provers},
+  crossref	= {odifreddi90},
+  pages		= {361-386},
+  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}
+
+% replaces paulson-ns and paulson-security
+@Article{paulson-jcs,
+  author	= {Lawrence C. Paulson},
+  title		= {The Inductive Approach to Verifying Cryptographic Protocols},
+  journal	= JCS,
+  year		= 1998,
+  volume	= 6,
+  pages		= {85-128}}
+
+@article{pelletier86,
+  author	= {F. J. Pelletier},
+  title		= {Seventy-five Problems for Testing Automatic Theorem
+		 Provers}, 
+  journal	= JAR,
+  volume	= 2,
+  pages		= {191-216},
+  year		= 1986,
+  note		= {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
+
+@Article{pitts94,  
+  author	= {Andrew M. Pitts},
+  title		= {A Co-induction Principle for Recursively Defined Domains},
+  journal	= TCS,
+  volume	= 124, 
+  pages		= {195-219},
+  year		= 1994} 
+
+@Article{plaisted90,
+  author	= {David A. Plaisted},
+  title		= {A Sequent-Style Model Elimination Strategy and a Positive
+		 Refinement},
+  journal	= JAR,
+  year		= 1990,
+  volume	= 6,
+  number	= 4,
+  pages		= {389-402}}
+
+%Q
+
+@Article{quaife92,
+  author	= {Art Quaife},
+  title		= {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
+		 Theory},
+  journal	= JAR,
+  year		= 1992,
+  volume	= 8,
+  number	= 1,
+  pages		= {91-147}}
+
+%R
+
+@TechReport{rasmussen95,
+  author	= {Ole Rasmussen},
+  title		= {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
+		  Experiment},
+  institution	= {Computer Laboratory, University of Cambridge},
+  year		= 1995,
+  number	= 364,
+  month		= may,
+  url		= {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}
+
+@Book{reeves90,
+  author	= {Steve Reeves and Michael Clarke},
+  title		= {Logic for Computer Science},
+  publisher	= {Addison-Wesley},
+  year		= 1990}
+
+%S
+
+@inproceedings{saaltink-fme,
+  author	= {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
+		 Dan Craigen and Irwin Meisels},
+  title		= {An {EVES} Data Abstraction Example}, 
+  pages		= {578-596},
+  crossref	= {fme93}}
+
+@inproceedings{slind-tfl,
+  author	= {Konrad Slind},
+  title		= {Function Definition in Higher Order Logic},
+  booktitle	= {Theorem Proving in Higher Order Logics},
+  editor	= {J. von Wright and J. Grundy and J. Harrison},
+  publisher	= Springer,
+  series	= LNCS,
+  volume	= 1125,
+  pages		= {381-397},
+  year		= 1996}
+
+@book{suppes72,
+  author	= {Patrick Suppes},
+  title		= {Axiomatic Set Theory},
+  year		= 1972,
+  publisher	= {Dover}}
+
+@InCollection{szasz93,
+  author	= {Nora Szasz},
+  title		= {A Machine Checked Proof that {Ackermann's} Function is not
+		  Primitive Recursive},
+  crossref	= {huet-plotkin93},
+  pages		= {317-338}}
+
+%T
+
+@book{takeuti87,
+  author	= {G. Takeuti},
+  title		= {Proof Theory},
+  year		= 1987,
+  publisher	= NH,
+  edition	= {2nd}}
+
+@Book{thompson91,
+  author	= {Simon Thompson},
+  title		= {Type Theory and Functional Programming},
+  publisher	= {Addison-Wesley},
+  year		= 1991}
+
+%V
+
+@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},
+  year		= 1994,
+  month		= aug}
+
+%W
+
+@book{principia,
+  author	= {A. N. Whitehead and B. Russell},
+  title		= {Principia Mathematica},
+  year		= 1962,
+  publisher	= CUP, 
+  note		= {Paperback edition to *56,
+  abridged from the 2nd edition (1927)}}
+
+@book{winskel93,
+  author	= {Glynn Winskel},
+  title		= {The Formal Semantics of Programming Languages},
+  publisher	= MIT,year=1993}
+
+@InCollection{wos-bledsoe,
+  author	= {Larry Wos},
+  title		= {Automated Reasoning and {Bledsoe's} Dream for the Field},
+  crossref	= {bledsoe-fest},
+  pages		= {297-342}}
+
+
+% CROSS REFERENCES
+
+@book{handbk-lics2,
+  editor	= {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
+  title		= {Handbook of Logic in Computer Science},
+  booktitle	= {Handbook of Logic in Computer Science},
+  publisher	= {Oxford University Press},
+  year		= 1992,
+  volume	= 2}
+
+@book{types93,
+  editor	= {Henk Barendregt and Tobias Nipkow},
+  title		= TYPES # {: International Workshop {TYPES '93}},
+  booktitle	= TYPES # {: International Workshop {TYPES '93}},
+  year		= {published 1994},
+  publisher	= {Springer},
+  series	= {LNCS 806}}
+
+@Proceedings{tlca93,
+  title		= {Typed Lambda Calculi and Applications},
+  booktitle	= {Typed Lambda Calculi and Applications},
+  editor	= {M. Bezem and J.F. Groote},
+  year		= 1993,
+  publisher	= {Springer},
+  series	= {LNCS 664}}
+
+@book{bledsoe-fest,
+  title		= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+  booktitle	= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+  publisher	= {Kluwer Academic Publishers},
+  year		= 1991,
+  editor	= {Robert S. Boyer}}
+
+@Proceedings{cade12,
+  editor	= {Alan Bundy},
+  title		= {Automated Deduction --- {CADE}-12 
+		  International Conference},
+  booktitle	= {Automated Deduction --- {CADE}-12 
+		  International Conference},
+  year		= 1994,
+  series	= {LNAI 814},
+  publisher	= {Springer}}
+
+@book{types94,
+  editor	= {Peter Dybjer and Bengt Nordstr{\"om} 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},
+  title		= {Logical Frameworks},
+  booktitle	= {Logical Frameworks},
+  publisher	= CUP,
+  year		= 1991}
+
+@proceedings{colog88,
+  editor	= {P. Martin-L\"of 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},
+  address	= {Tallinn},
+  series	= {LNCS 417}}
+
+@book{odifreddi90,
+  editor	= {P. Odifreddi},
+  title		= {Logic and Computer Science},
+  booktitle	= {Logic and Computer Science},
+  publisher	= {Academic Press},
+  year		= 1990}
+
+@proceedings{extensions91,
+  editor	= {Peter Schroeder-Heister},
+  title		= {Extensions of Logic Programming},
+  booktitle	= {Extensions of Logic Programming},
+  year		= 1991,
+  series	= {LNAI 475}, 
+  publisher	= {Springer}}
+
+@proceedings{cade10,
+  editor	= {Mark E. Stickel},
+  title		= {10th } # CADE,
+  booktitle	= {10th } # CADE,
+  year		= 1990,
+  publisher	= {Springer},
+  series	= {LNAI 449}}
+
+@Proceedings{lics8,
+  editor	= {M. Vardi},
+  title		= {Eighth Annual Symposium on Logic in Computer Science},
+  booktitle	= {Eighth Annual Symposium on Logic in Computer Science},
+  publisher	= IEEE,
+  year		= 1993}
+
+@book{wos-fest,
+  title		= {Automated Reasoning and its Applications: 
+			Essays in Honor of {Larry Wos}},
+  booktitle	= {Automated Reasoning and its Applications: 
+			Essays in Honor of {Larry Wos}},
+  publisher	= {MIT Press},
+  year		= 1997,
+  editor	= {Robert Veroff}}
+
+@Proceedings{tphols96,
+  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
+  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
+  editor	= {J. von Wright and J. Grundy and J. Harrison},
+  series	= {LNCS 1125},
+  year		= 1996}