--- a/src/Doc/manual.bib Fri Sep 25 20:37:59 2015 +0200
+++ b/src/Doc/manual.bib Fri Sep 25 23:39:08 2015 +0200
@@ -601,6 +601,17 @@
year = 1993,
pages = {213-248}}
+@article{Farmer:2008,
+ author = {William M. Farmer},
+ title = {The seven virtues of simple type theory},
+ journal = {J. Applied Logic},
+ volume = {6},
+ number = {3},
+ pages = {267--286},
+ year = {2008},
+ url = {http://dx.doi.org/10.1016/j.jal.2007.11.001},
+}
+
@InProceedings{felty91a,
Author = {Amy Felty},
Title = {A Logic Program for Transforming Sequent Proofs to Natural
@@ -679,6 +690,14 @@
publisher = CUP,
note = {Translated by Yves Lafont and Paul Taylor}}
+@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
+}
+
@Book{mgordon-hol,
editor = {M. J. C. Gordon and T. F. Melham},
title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
@@ -978,6 +997,20 @@
note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
}
+@inproceedings{Kuncar-Popescu:2015,
+ author = {Ondrej Kuncar and Andrei Popescu},
+ title = {A Consistent Foundation for {Isabelle/HOL}},
+ editor = {Christian Urban and Xingyuan Zhang},
+ booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
+ 2015, Nanjing, China, August 24-27, 2015, Proceedings},
+ year = {2015},
+ url = {http://dx.doi.org/10.1007/978-3-319-22102-1_16},
+ series = {Lecture Notes in Computer Science},
+ volume = {9236},
+ publisher = {Springer},
+ year = {2015},
+}
+
@Book{kunen80,
author = {Kenneth Kunen},
title = {Set Theory: An Introduction to Independence Proofs},