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