doc-src/IsarRef/isar-ref.tex
author wenzelm
Sun Sep 18 14:25:53 2011 +0200 (2011-09-18)
changeset 44966 1db165e0bd97
parent 42917 ba23e83b0868
child 47860 fa7f5755b27a
permissions -rw-r--r--
more contributors;
     1 \documentclass[12pt,a4paper,fleqn]{report}
     2 \usepackage{amssymb}
     3 \usepackage[greek,english]{babel}
     4 \usepackage[only,bigsqcap]{stmaryrd}
     5 \usepackage{textcomp}
     6 \usepackage{latexsym}
     7 \usepackage{graphicx}
     8 \let\intorig=\int  %iman.sty redefines \int
     9 \usepackage{../iman,../extra,../isar,../proof}
    10 \usepackage[nohyphen,strings]{../underscore}
    11 \usepackage{../../lib/texinputs/isabelle}
    12 \usepackage{../../lib/texinputs/isabellesym}
    13 \usepackage{../../lib/texinputs/railsetup}
    14 \usepackage{../ttbox}
    15 \usepackage{supertabular}
    16 \usepackage{style}
    17 \usepackage{../pdfsetup}
    18 
    19 \hyphenation{Isabelle}
    20 \hyphenation{Isar}
    21 
    22 \isadroptag{theory}
    23 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    24 \author{\emph{Makarius Wenzel} \\[3ex]
    25   With Contributions by
    26   Clemens Ballarin,
    27   Stefan Berghofer, \\
    28   Jasmin Blanchette,
    29   Timothy Bourke,
    30   Lukas Bulwahn, \\
    31   Lucas Dixon,
    32   Florian Haftmann,
    33   Gerwin Klein, \\
    34   Alexander Krauss,
    35   Tobias Nipkow,
    36   Lars Noschinski, \\
    37   David von Oheimb,
    38   Larry Paulson,
    39   Sebastian Skalberg
    40 }
    41 
    42 \makeindex
    43 
    44 \chardef\charbackquote=`\`
    45 \newcommand{\backquote}{\mbox{\tt\charbackquote}}
    46 
    47 
    48 \begin{document}
    49 
    50 \maketitle 
    51 
    52 \pagenumbering{roman}
    53 {\def\isamarkupchapter#1{\chapter*{#1}}\input{Thy/document/Preface.tex}}
    54 \tableofcontents
    55 \clearfirst
    56 
    57 \part{Basic Concepts}
    58 \input{Thy/document/Synopsis.tex}
    59 \input{Thy/document/Framework.tex}
    60 \input{Thy/document/First_Order_Logic.tex}
    61 \part{General Language Elements}
    62 \input{Thy/document/Outer_Syntax.tex}
    63 \input{Thy/document/Document_Preparation.tex}
    64 \input{Thy/document/Spec.tex}
    65 \input{Thy/document/Proof.tex}
    66 \input{Thy/document/Inner_Syntax.tex}
    67 \input{Thy/document/Misc.tex}
    68 \input{Thy/document/Generic.tex}
    69 \part{Object-Logics}
    70 \input{Thy/document/HOL_Specific.tex}
    71 \input{Thy/document/HOLCF_Specific.tex}
    72 \input{Thy/document/ZF_Specific.tex}
    73 
    74 \part{Appendix}
    75 \appendix
    76 \input{Thy/document/Quick_Reference.tex}
    77 \let\int\intorig
    78 \input{Thy/document/Symbols.tex}
    79 \input{Thy/document/ML_Tactic.tex}
    80 
    81 \begingroup
    82   \bibliographystyle{abbrv} \small\raggedright\frenchspacing
    83   \bibliography{../manual}
    84 \endgroup
    85 
    86 \printindex
    87 
    88 \end{document}