wneuper/isa: doc-src/IsarRef/isar-ref.tex@1db165e0bd97

     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}

    19 \hyphenation{Isabelle}

    20 \hyphenation{Isar}

    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 }

    42 \makeindex

    44 \chardef\charbackquote=`\`

    45 \newcommand{\backquote}{\mbox{\tt\charbackquote}}

    48 \begin{document}

    50 \maketitle

    52 \pagenumbering{roman}

    53 {\def\isamarkupchapter#1{\chapter*{#1}}\input{Thy/document/Preface.tex}}

    54 \tableofcontents

    55 \clearfirst

    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}

    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}

    81 \begingroup

    82   \bibliographystyle{abbrv} \small\raggedright\frenchspacing

    83   \bibliography{../manual}

    84 \endgroup

    86 \printindex

    88 \end{document}

author	wenzelm
	Sun, 18 Sep 2011 14:25:53 +0200
changeset 45837	1db165e0bd97
parent 44121	ba23e83b0868
child 48731	fa7f5755b27a
permissions	-rw-r--r--