src/HOL/Real/ex/document/root.tex
changeset 16422 9aa6d9cf2832
parent 16421 650ef3c13c4d
child 16423 24abe4c0e4b4
equal deleted inserted replaced
16421:650ef3c13c4d 16422:9aa6d9cf2832
     1 
       
     2 \documentclass[11pt,a4paper]{article}
       
     3 \usepackage[latin1]{inputenc}
       
     4 \usepackage{isabelle,isabellesym}
       
     5 \usepackage{pdfsetup}
       
     6 
       
     7 \urlstyle{rm}
       
     8 \isabellestyle{it}
       
     9 
       
    10 \begin{document}
       
    11 
       
    12 \title{Miscellaneous HOL-Real Examples}
       
    13 \maketitle
       
    14 
       
    15 \tableofcontents
       
    16 
       
    17 \parindent 0pt\parskip 0.5ex
       
    18 \input{session}
       
    19 
       
    20 \end{document}