# HG changeset patch
# User haftmann
# Date 1214467614 -7200
# Node ID a75d71c733628ff8e601eb6a81df40b911740c33
# Parent  d0cda1ea705e3625aa8f8e29d16e3d05b099d8d7
added dummy citiation

diff -r d0cda1ea705e -r a75d71c73362 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Jun 26 10:06:53 2008 +0200
+++ b/src/HOL/Main.thy	Thu Jun 26 10:06:54 2008 +0200
@@ -5,11 +5,11 @@
 header {* Main HOL *}
 
 theory Main
-imports Map
+imports Plain Map Presburger Recdef
 begin
 
 ML {* val HOL_proofs = ! Proofterm.proofs *}
 
-ML {* path_add "~~/src/HOL/Library" *}
+text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
 end
diff -r d0cda1ea705e -r a75d71c73362 src/HOL/document/root.bib
--- a/src/HOL/document/root.bib	Thu Jun 26 10:06:53 2008 +0200
+++ b/src/HOL/document/root.bib	Thu Jun 26 10:06:54 2008 +0200
@@ -1,3 +1,16 @@
 
-@book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
-publisher={American Mathematical Society},year=1979}
\ No newline at end of file
+@book{Birkhoff79,
+  author =      {Garret Birkhoff},
+  title =       {Lattice Theory},
+  publisher =   {American Mathematical Society},
+  year=1979
+}
+
+@book{Nipkow-et-al:2002:tutorial,
+  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
+  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
+  series =      {LNCS},
+  volume =      2283,
+  year =        2002,
+  publisher =   {Springer-Verlag}
+}
\ No newline at end of file