wneuper/isa: doc-src/IsarRef/isar-ref.tex@2b75760fa75e

     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   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 }

    39 \makeindex

    41 \chardef\charbackquote=`\`

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

    45 \begin{document}

    47 \maketitle

    49 \pagenumbering{roman}

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

    51 \tableofcontents

    52 \clearfirst

    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}

    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}

    78 \begingroup

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

    80   \bibliography{../manual}

    81 \endgroup

    83 \printindex

    85 \end{document}

author	blanchet
	Thu, 28 Jul 2011 16:32:39 +0200
changeset 44872	2b75760fa75e
parent 44121	ba23e83b0868
child 45837	1db165e0bd97
permissions	-rw-r--r--