doc-src/IsarRef/isar-ref.tex
author haftmann
Wed Sep 07 23:38:52 2011 +0200 (2011-09-07)
changeset 44818 27ba81ad0890
parent 42917 ba23e83b0868
child 44966 1db165e0bd97
permissions -rw-r--r--
theory of saturated naturals contributed by Peter Gammie
     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   Timothy Bourke,
    29   Lucas Dixon,
    30   Florian Haftmann, \\
    31   Gerwin Klein,
    32   Alexander Krauss,
    33   Tobias Nipkow, \\
    34   David von Oheimb,
    35   Larry Paulson,
    36   and Sebastian Skalberg
    37 }
    38 
    39 \makeindex
    40 
    41 \chardef\charbackquote=`\`
    42 \newcommand{\backquote}{\mbox{\tt\charbackquote}}
    43 
    44 
    45 \begin{document}
    46 
    47 \maketitle 
    48 
    49 \pagenumbering{roman}
    50 {\def\isamarkupchapter#1{\chapter*{#1}}\input{Thy/document/Preface.tex}}
    51 \tableofcontents
    52 \clearfirst
    53 
    54 \part{Basic Concepts}
    55 \input{Thy/document/Synopsis.tex}
    56 \input{Thy/document/Framework.tex}
    57 \input{Thy/document/First_Order_Logic.tex}
    58 \part{General Language Elements}
    59 \input{Thy/document/Outer_Syntax.tex}
    60 \input{Thy/document/Document_Preparation.tex}
    61 \input{Thy/document/Spec.tex}
    62 \input{Thy/document/Proof.tex}
    63 \input{Thy/document/Inner_Syntax.tex}
    64 \input{Thy/document/Misc.tex}
    65 \input{Thy/document/Generic.tex}
    66 \part{Object-Logics}
    67 \input{Thy/document/HOL_Specific.tex}
    68 \input{Thy/document/HOLCF_Specific.tex}
    69 \input{Thy/document/ZF_Specific.tex}
    70 
    71 \part{Appendix}
    72 \appendix
    73 \input{Thy/document/Quick_Reference.tex}
    74 \let\int\intorig
    75 \input{Thy/document/Symbols.tex}
    76 \input{Thy/document/ML_Tactic.tex}
    77 
    78 \begingroup
    79   \bibliographystyle{abbrv} \small\raggedright\frenchspacing
    80   \bibliography{../manual}
    81 \endgroup
    82 
    83 \printindex
    84 
    85 \end{document}