--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/document/root.bib Fri Dec 29 18:09:38 2017 +0100
@@ -0,0 +1,10 @@
+@string{CUCL="Computer Laboratory, University of Cambridge"}
+
+@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}
--- a/src/ZF/Induct/document/root.bib Fri Dec 29 17:40:57 2017 +0100
+++ b/src/ZF/Induct/document/root.bib Fri Dec 29 18:09:38 2017 +0100
@@ -1,3 +1,15 @@
+@string{CUCL="Computer Laboratory, University of Cambridge"}
+@string{CUP="Cambridge University Press"}
+
+@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}
+
@InProceedings{paulin-tlca,
author = {Christine Paulin-Mohring},
title = {Inductive Definitions in the System {Coq}: Rules and