wneuper/isa: doc-src/IsarRef/isar-ref.tex@72197611f1e9

     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   Brian Huffman, \\

    34   Gerwin Klein,

    35   Alexander Krauss,

    36   Ond\v{r}ej Kun\v{c}ar, \\

    37   Tobias Nipkow,

    38   Lars Noschinski,

    39   David von Oheimb, \\

    40   Larry Paulson,

    41   Sebastian Skalberg

    42 }

    44 \makeindex

    46 \chardef\charbackquote=`\`

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

    50 \begin{document}

    52 \maketitle

    54 \pagenumbering{roman}

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

    56 \tableofcontents

    57 \clearfirst

    59 \part{Basic Concepts}

    60 \input{Thy/document/Synopsis.tex}

    61 \input{Thy/document/Framework.tex}

    62 \input{Thy/document/First_Order_Logic.tex}

    63 \part{General Language Elements}

    64 \input{Thy/document/Outer_Syntax.tex}

    65 \input{Thy/document/Document_Preparation.tex}

    66 \input{Thy/document/Spec.tex}

    67 \input{Thy/document/Proof.tex}

    68 \input{Thy/document/Inner_Syntax.tex}

    69 \input{Thy/document/Misc.tex}

    70 \input{Thy/document/Generic.tex}

    71 \part{Object-Logics}

    72 \input{Thy/document/HOL_Specific.tex}

    73 \input{Thy/document/HOLCF_Specific.tex}

    74 \input{Thy/document/ZF_Specific.tex}

    76 \part{Appendix}

    77 \appendix

    78 \input{Thy/document/Quick_Reference.tex}

    79 \let\int\intorig

    80 \input{Thy/document/Symbols.tex}

    81 \input{Thy/document/ML_Tactic.tex}

    83 \begingroup

    84   \tocentry{\bibname}

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

    86   \bibliography{../manual}

    87 \endgroup

    89 \tocentry{\indexname}

    90 \printindex

    92 \end{document}

author	wenzelm
	Fri, 01 Jun 2012 13:39:14 +0200
changeset 49072	72197611f1e9
parent 48731	fa7f5755b27a
child 49186	28a6d67c93f0
permissions	-rw-r--r--