--- 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}},