src/HOL/Docs/document/root.tex

--- a/src/HOL/Docs/document/root.tex	Wed Mar 11 11:41:14 2009 +0100
+++ b/src/HOL/Docs/document/root.tex	Wed Mar 11 12:51:00 2009 +0100
@@ -53,22 +53,13 @@
 
 \title{What's in Main}
 \author{Tobias Nipkow}
-\date{}
+\date{\today}
 \maketitle
 
-%\setcounter{tocdepth}{1}
-%\tableofcontents
-
-% generated text of all theories
-\input{session}
+\input{Main_Doc}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: