wneuper/isa: doc-src/IsarRef/isar-ref.tex@28a6d67c93f0

     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}

    20 \hyphenation{Isabelle}

    21 \hyphenation{Isar}

    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 }

    45 \makeindex

    47 \chardef\charbackquote=`\`

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

    51 \begin{document}

    53 \maketitle

    55 \pagenumbering{roman}

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

    57 \tableofcontents

    58 \clearfirst

    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}

    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}

    84 \begingroup

    85   \tocentry{\bibname}

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

    87   \bibliography{../manual}

    88 \endgroup

    90 \tocentry{\indexname}

    91 \printindex

    93 \end{document}

author	wenzelm
	Fri, 29 Jun 2012 15:45:50 +0200
changeset 49186	28a6d67c93f0
parent 49072	72197611f1e9
child 49971	d54a3d39ba85
permissions	-rw-r--r--