diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Isar_Examples/document/root.bib
--- a/src/HOL/Isar_Examples/document/root.bib	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.bib	Sat Dec 26 19:27:46 2015 +0100
@@ -44,6 +44,14 @@
   publisher	= CUP,
   year		= 1990}
 
+@TechReport{Gordon:1985:HOL,
+  author =       {M. J. C. Gordon},
+  title =        {{HOL}: A machine oriented formulation of higher order logic},
+  institution =  {University of Cambridge Computer Laboratory},
+  year =         1985,
+  number =       68
+}
+
 @manual{isabelle-HOL,
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   title		= {{Isabelle}'s Logics: {HOL}},