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