bib;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/document/root.bib	Sat Oct 09 23:17:47 1999 +0200
@@ -0,0 +1,41 @@
+
+@string{CUCL="Comp. Lab., Univ. Camb."}
+@string{CUP="Cambridge University Press"}
+@string{Springer="Springer-Verlag"}
+@string{TUM="TU Munich"}
+
+
+@Book{davey-priestley,
+  author	= {B. A. Davey and H. A. Priestley},
+  title		= {Introduction to Lattices and Order},
+  publisher	= CUP,
+  year		= 1990}
+
+@manual{isabelle-HOL,
+  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  title		= {{Isabelle}'s Logics: {HOL}},
+  institution	= {Institut f\"ur Informatik, Technische Universi\"at
+                  M\"unchen and Computer Laboratory, University of Cambridge}}
+
+@manual{isabelle-intro,
+  author	= {Lawrence C. Paulson},
+  title		= {Introduction to {Isabelle}},
+  institution	= CUCL}
+
+@manual{isabelle-isar-ref,
+  author	= {Markus Wenzel},
+  title		= {The {Isabelle Isar} Reference Manual},
+  institution	= TUM}
+
+@InProceedings{Wenzel:1999:TPHOL,
+  author = 	 {Markus Wenzel},
+  title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+  crossref =     {tphols99}}
+
+@Proceedings{tphols99,
+  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+  editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
+                  Paulin, C. and Thery, L.},
+  series	= {LNCS 1690},
+  year		= 1999}

--- a/src/HOL/Isar_examples/document/root.tex	Sat Oct 09 23:16:59 1999 +0200
+++ b/src/HOL/Isar_examples/document/root.tex	Sat Oct 09 23:17:47 1999 +0200
@@ -19,4 +19,8 @@
 \tableofcontents
 \input{session}
 
+\nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
+\bibliographystyle{plain}
+\bibliography{root}
+
 \end{document}