doc-src/System/system.tex
changeset 28216 5423ad29648e
parent 27639 83e6a4c43d17
child 28219 5465883d64da
equal deleted inserted replaced
28215:a1cfc43ac47d 28216:5423ad29648e
     7 \usepackage[latin1]{inputenc}
     7 \usepackage[latin1]{inputenc}
     8 \usepackage[only,bigsqcap]{stmaryrd}
     8 \usepackage[only,bigsqcap]{stmaryrd}
     9 \usepackage{textcomp}
     9 \usepackage{textcomp}
    10 \usepackage{supertabular}
    10 \usepackage{supertabular}
    11 \let\intorig=\int  %iman.sty redefines \int
    11 \let\intorig=\int  %iman.sty redefines \int
    12 \usepackage{graphicx,../iman,../extra,../ttbox,../isabelle,../isabellesym,../pdfsetup}
    12 \usepackage[nohyphen,strings]{../underscore}
       
    13 \usepackage{graphicx}
       
    14 \usepackage{../iman,../extra,../isar,../ttbox}
       
    15 \usepackage{../isabelle,../isabellesym}
       
    16 \usepackage{../IsarRef/style}
       
    17 \usepackage{../pdfsetup}
       
    18 
       
    19 \hyphenation{Isabelle}
       
    20 \hyphenation{Isar}
       
    21 
       
    22 \isadroptag{theory}
    13 
    23 
    14 \isabellestyle{it}
    24 \isabellestyle{it}
    15 
    25 
    16 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
    26 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
    17 
    27 
    18 \author{\emph{Markus Wenzel} and \emph{Stefan Berghofer} \\
    28 \author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\
    19   TU M\"unchen}
    29   TU M\"unchen}
    20 
    30 
    21 \makeindex
    31 \makeindex
    22 
    32 
    23 \setcounter{secnumdepth}{1} \setcounter{tocdepth}{2}
       
    24 
       
    25 \pagestyle{headings}
       
    26 \sloppy
       
    27 \binperiod     %%%treat . like a binary operator
       
    28 
    33 
    29 \begin{document}
    34 \begin{document}
    30 
       
    31 \underscoreoff
       
    32 
    35 
    33 \maketitle 
    36 \maketitle 
    34 \pagenumbering{roman} \tableofcontents \clearfirst
    37 \pagenumbering{roman} \tableofcontents \clearfirst
    35 
    38 
    36 \include{basics}
    39 \input{Thy/document/Basics}
    37 \include{present}
    40 \input{present}
    38 \include{misc}
    41 \input{misc}
    39 
    42 
    40 \appendix
    43 \appendix
    41 \let\int\intorig
    44 \let\int\intorig
    42 \include{symbols}
    45 \input{symbols}
    43 
    46 
    44 \begingroup
    47 \begingroup
    45   \bibliographystyle{plain} \small\raggedright\frenchspacing
    48   \bibliographystyle{plain} \small\raggedright\frenchspacing
    46   \bibliography{../manual}
    49   \bibliography{../manual}
    47 \endgroup
    50 \endgroup