# HG changeset patch
# User wenzelm
# Date 1514567378 -3600
# Node ID fee3ed06a281cc16b2b9bb2ab00e84570afb6b1e
# Parent  86a099f896fc42c457378f337b668a1c5ea0686a
proper bibtex entries;

diff -r 86a099f896fc -r fee3ed06a281 src/HOL/Induct/document/root.bib
--- /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}
diff -r 86a099f896fc -r fee3ed06a281 src/ZF/Induct/document/root.bib
--- 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