src/ZF/Induct/document/root.bib
author immler
Sun, 27 Oct 2019 21:51:14 -0400
changeset 71035 6fe5a0e1fa8e
parent 67298 fee3ed06a281
permissions -rw-r--r--
moved theory Interval from the AFP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67298
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     1
@string{CUCL="Computer Laboratory, University of Cambridge"}
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     2
@string{CUP="Cambridge University Press"}
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     3
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     4
@TechReport{camilleri92,
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     5
  author	= {J. Camilleri and T. F. Melham},
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     6
  title		= {Reasoning with Inductively Defined Relations in the
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     7
		 {HOL} Theorem Prover},
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     8
  institution	= CUCL,
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
     9
  year		= 1992,
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
    10
  number	= 265,
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
    11
  month		= Aug}
fee3ed06a281 proper bibtex entries;
wenzelm
parents: 58638
diff changeset
    12
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    13
@InProceedings{paulin-tlca,
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    14
  author	= {Christine Paulin-Mohring},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    15
  title		= {Inductive Definitions in the System {Coq}: Rules and
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    16
		 Properties},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    17
  crossref	= {tlca93},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    18
  pages		= {328-345}}
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    19
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    20
@Proceedings{tlca93,
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    21
  title		= {Typed Lambda Calculi and Applications},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    22
  booktitle	= {Typed Lambda Calculi and Applications},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    23
  editor	= {M. Bezem and J.F. Groote},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    24
  year		= 1993,
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    25
  publisher	= {Springer},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    26
  series	= {LNCS 664}}
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    27
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    28
@InCollection{szasz93,
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    29
  author	= {Nora Szasz},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    30
  title		= {A Machine Checked Proof that {Ackermann's} Function is not
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    31
		  Primitive Recursive},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    32
  crossref	= {huet-plotkin93},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    33
  pages		= {317-338}}
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    34
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    35
@book{huet-plotkin93,
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    36
  editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    37
  title		= {Logical Environments},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    38
  booktitle	= {Logical Environments},
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    39
  publisher	= CUP,
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    40
  year		= 1993}
2db1df2c8467 more bibtex entries;
wenzelm
parents:
diff changeset
    41
58638
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    42
@book{mendelson,
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    43
  Author = {E. Mendelson},
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    44
  Edition = {Fourth},
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    45
  Publisher = {Chapman \& Hall},
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    46
  Title = {Introduction to Mathematical Logic},
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    47
  Year = {1997}}
5855b9b3d6a3 proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents: 58623
diff changeset
    48