1@string{CUCL="Computer Laboratory, University of Cambridge"}
2@string{CUP="Cambridge University Press"}
3
4@TechReport{camilleri92,
5  author	= {J. Camilleri and T. F. Melham},
6  title		= {Reasoning with Inductively Defined Relations in the
7		 {HOL} Theorem Prover},
8  institution	= CUCL,
9  year		= 1992,
10  number	= 265,
11  month		= Aug}
12
13@InProceedings{paulin-tlca,
14  author	= {Christine Paulin-Mohring},
15  title		= {Inductive Definitions in the System {Coq}: Rules and
16		 Properties},
17  crossref	= {tlca93},
18  pages		= {328-345}}
19
20@Proceedings{tlca93,
21  title		= {Typed Lambda Calculi and Applications},
22  booktitle	= {Typed Lambda Calculi and Applications},
23  editor	= {M. Bezem and J.F. Groote},
24  year		= 1993,
25  publisher	= {Springer},
26  series	= {LNCS 664}}
27
28@InCollection{szasz93,
29  author	= {Nora Szasz},
30  title		= {A Machine Checked Proof that {Ackermann's} Function is not
31		  Primitive Recursive},
32  crossref	= {huet-plotkin93},
33  pages		= {317-338}}
34
35@book{huet-plotkin93,
36  editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
37  title		= {Logical Environments},
38  booktitle	= {Logical Environments},
39  publisher	= CUP,
40  year		= 1993}
41
42@book{mendelson,
43  Author = {E. Mendelson},
44  Edition = {Fourth},
45  Publisher = {Chapman \& Hall},
46  Title = {Introduction to Mathematical Logic},
47  Year = {1997}}
48
49