--- a/src/HOL/ex/document/root.bib Fri Aug 02 21:40:28 2002 +0200
+++ b/src/HOL/ex/document/root.bib Fri Aug 02 21:40:47 2002 +0200
@@ -48,6 +48,15 @@
pages = {363--397}
}
+@Book{Paulson:1994:Isabelle,
+ author = {L. C. Paulson and T. Nipkow},
+ title = {{Isabelle}: A Generic Theorem Prover},
+ year = 1994,
+ series = {LNCS},
+ volume = {828},
+ publisher = {Springer}
+}
+
@InProceedings{Wenzel:1999,
author = {Markus Wenzel},
title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
@@ -66,6 +75,7 @@
note = {Part of the Isabelle distribution,
\url{http://isabelle.in.tum.de/library/HOL/Isar_examples/document.pdf}}
}
+
@PhdThesis{Wenzel:2001:Thesis,
author = {Markus Wenzel},
title = {Isabelle/Isar --- a versatile environment for human-readable
@@ -75,7 +85,6 @@
month = {September},
note = {Submitted}
}
-
@Manual{Wenzel:2001:isar-ref,
author = {Markus Wenzel},
title = {The {Isabelle/Isar} Reference Manual},
@@ -84,3 +93,10 @@
note = {Part of the Isabelle distribution,
\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
}
+
+@Book{isabelle-hol-book,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+ publisher = {Springer},
+ year = 2002,
+ note = {LNCS 2283}}