src/HOL/Docs/document/root.tex
changeset 30442 1bc0638d554d
parent 30440 5f47d3cb781a
equal deleted inserted replaced
30441:193cf2fa692a 30442:1bc0638d554d
    51 
    51 
    52 \begin{document}
    52 \begin{document}
    53 
    53 
    54 \title{What's in Main}
    54 \title{What's in Main}
    55 \author{Tobias Nipkow}
    55 \author{Tobias Nipkow}
    56 \date{}
    56 \date{\today}
    57 \maketitle
    57 \maketitle
    58 
    58 
    59 %\setcounter{tocdepth}{1}
    59 \input{Main_Doc}
    60 %\tableofcontents
       
    61 
       
    62 % generated text of all theories
       
    63 \input{session}
       
    64 
    60 
    65 % optional bibliography
    61 % optional bibliography
    66 %\bibliographystyle{abbrv}
    62 %\bibliographystyle{abbrv}
    67 %\bibliography{root}
    63 %\bibliography{root}
    68 
    64 
    69 \end{document}
    65 \end{document}
    70 
       
    71 %%% Local Variables:
       
    72 %%% mode: latex
       
    73 %%% TeX-master: t
       
    74 %%% End: