doc-src/IsarRef/isar-ref.tex
author wenzelm
Tue May 31 22:47:18 2011 +0200 (2011-05-31)
changeset 42917 ba23e83b0868
parent 42915 f35aae36cad0
child 44966 1db165e0bd97
permissions -rw-r--r--
added Synopsis, with some "Notepad" material;
     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}