ex/document/root.bib;

--- a/src/HOL/IsaMakefile	Thu Nov 08 00:26:41 2001 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 08 17:42:43 2001 +0100
@@ -532,7 +532,7 @@
   ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/Tarski.ML \
   ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \
   ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy \
-  ex/document/root.tex
+  ex/document/root.bib ex/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/document/root.bib	Thu Nov 08 17:42:43 2001 +0100
@@ -0,0 +1,60 @@
+
+@InProceedings{Kamm-et-al:1999,
+  author =       {Florian Kamm{\"u}ller and Markus Wenzel and
+                  Lawrence C. Paulson},
+  title =        {Locales: A Sectioning Concept for {Isabelle}},
+  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},
+  volume        = 1690,
+  year          = 1999}
+
+@InProceedings{Naraschewski-Wenzel:1998,
+  author        = {Wolfgang Naraschewski and Markus Wenzel},
+  title         = {Object-Oriented Verification based on Record Subtyping in
+                  {H}igher-{O}rder {L}ogic},
+  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+  editor        = {Jim Grundy and Malcom Newey},
+  series        = {LNCS},
+  volume        = 1479,
+  year          = 1998}
+
+@Manual{Nipkow-et-al:2001:HOL,
+  author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  title         = {{Isabelle}'s Logics: {HOL}},
+  institution   = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
+                  M{\"u}nchen and Computer Laboratory, University of Cambridge},
+  year          = 2001,
+  note          = {Part of the Isabelle distribution,
+                   \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
+}
+
+@InProceedings{Wenzel:1999,
+  author =       {Markus Wenzel},
+  title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+  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},
+  volume        = 1690,
+  year          = 1999}
+
+@PhdThesis{Wenzel:2001:Thesis,
+  author = 	 {Markus Wenzel},
+  title = 	 {Isabelle/Isar --- a versatile environment for human-readable
+                  formal proof documents},
+  school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
+  year = 	 2001,
+  month =	 {September},
+  note =	 {Submitted}
+}
+
+@Manual{Wenzel:2001:isar-ref,
+  author        = {Markus Wenzel},
+  title         = {The {Isabelle/Isar} Reference Manual},
+  year          = 2001,
+  institution   = {TU M{\"u}nchen},
+  note          = {Part of the Isabelle distribution,
+                   \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
+}