doc-src/IsarRef/isar-ref.tex
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 48171 28a6d67c93f0
child 48956 d54a3d39ba85
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
wenzelm@7836
     1
\documentclass[12pt,a4paper,fleqn]{report}
wenzelm@28838
     2
\usepackage{amssymb}
wenzelm@48171
     3
\usepackage{eurosym}
wenzelm@48171
     4
\usepackage[english]{babel}
wenzelm@28838
     5
\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@28838
     6
\usepackage{textcomp}
wenzelm@28838
     7
\usepackage{latexsym}
wenzelm@28838
     8
\usepackage{graphicx}
wenzelm@28838
     9
\let\intorig=\int  %iman.sty redefines \int
wenzelm@26738
    10
\usepackage{../iman,../extra,../isar,../proof}
wenzelm@26862
    11
\usepackage[nohyphen,strings]{../underscore}
wenzelm@42632
    12
\usepackage{../../lib/texinputs/isabelle}
wenzelm@42632
    13
\usepackage{../../lib/texinputs/isabellesym}
wenzelm@42632
    14
\usepackage{../../lib/texinputs/railsetup}
wenzelm@42632
    15
\usepackage{../ttbox}
wenzelm@28773
    16
\usepackage{supertabular}
wenzelm@26738
    17
\usepackage{style}
wenzelm@26738
    18
\usepackage{../pdfsetup}
wenzelm@7046
    19
wenzelm@26741
    20
\hyphenation{Isabelle}
wenzelm@26741
    21
\hyphenation{Isar}
wenzelm@26741
    22
wenzelm@26741
    23
\isadroptag{theory}
wenzelm@7046
    24
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
wenzelm@26870
    25
\author{\emph{Makarius Wenzel} \\[3ex]
wenzelm@26870
    26
  With Contributions by
wenzelm@26870
    27
  Clemens Ballarin,
wenzelm@26870
    28
  Stefan Berghofer, \\
wenzelm@44966
    29
  Jasmin Blanchette,
haftmann@30569
    30
  Timothy Bourke,
wenzelm@44966
    31
  Lukas Bulwahn, \\
wenzelm@27038
    32
  Lucas Dixon,
wenzelm@44966
    33
  Florian Haftmann,
wenzelm@47860
    34
  Brian Huffman, \\
wenzelm@47860
    35
  Gerwin Klein,
wenzelm@27038
    36
  Alexander Krauss,
wenzelm@47860
    37
  Ond\v{r}ej Kun\v{c}ar, \\
wenzelm@44966
    38
  Tobias Nipkow,
wenzelm@47860
    39
  Lars Noschinski,
wenzelm@47860
    40
  David von Oheimb, \\
wenzelm@27038
    41
  Larry Paulson,
wenzelm@44966
    42
  Sebastian Skalberg
wenzelm@26870
    43
}
wenzelm@7046
    44
wenzelm@7050
    45
\makeindex
wenzelm@7050
    46
wenzelm@18021
    47
\chardef\charbackquote=`\`
wenzelm@18021
    48
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
wenzelm@18021
    49
wenzelm@7046
    50
wenzelm@7046
    51
\begin{document}
wenzelm@7046
    52
wenzelm@7046
    53
\maketitle 
wenzelm@7046
    54
wenzelm@42915
    55
\pagenumbering{roman}
wenzelm@42915
    56
{\def\isamarkupchapter#1{\chapter*{#1}}\input{Thy/document/Preface.tex}}
wenzelm@42915
    57
\tableofcontents
wenzelm@42915
    58
\clearfirst
wenzelm@7046
    59
wenzelm@29718
    60
\part{Basic Concepts}
wenzelm@42917
    61
\input{Thy/document/Synopsis.tex}
wenzelm@29716
    62
\input{Thy/document/Framework.tex}
wenzelm@29730
    63
\input{Thy/document/First_Order_Logic.tex}
wenzelm@29718
    64
\part{General Language Elements}
wenzelm@27037
    65
\input{Thy/document/Outer_Syntax.tex}
wenzelm@28751
    66
\input{Thy/document/Document_Preparation.tex}
wenzelm@26869
    67
\input{Thy/document/Spec.tex}
wenzelm@26869
    68
\input{Thy/document/Proof.tex}
wenzelm@28762
    69
\input{Thy/document/Inner_Syntax.tex}
wenzelm@27048
    70
\input{Thy/document/Misc.tex}
wenzelm@26782
    71
\input{Thy/document/Generic.tex}
wenzelm@29718
    72
\part{Object-Logics}
wenzelm@26840
    73
\input{Thy/document/HOL_Specific.tex}
wenzelm@26840
    74
\input{Thy/document/HOLCF_Specific.tex}
wenzelm@26840
    75
\input{Thy/document/ZF_Specific.tex}
wenzelm@7046
    76
wenzelm@29718
    77
\part{Appendix}
wenzelm@7895
    78
\appendix
wenzelm@26779
    79
\input{Thy/document/Quick_Reference.tex}
wenzelm@28838
    80
\let\int\intorig
wenzelm@28838
    81
\input{Thy/document/Symbols.tex}
wenzelm@26846
    82
\input{Thy/document/ML_Tactic.tex}
wenzelm@7895
    83
wenzelm@7046
    84
\begingroup
wenzelm@48057
    85
  \tocentry{\bibname}
wenzelm@30116
    86
  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
wenzelm@7046
    87
  \bibliography{../manual}
wenzelm@7046
    88
\endgroup
wenzelm@7046
    89
wenzelm@48057
    90
\tocentry{\indexname}
wenzelm@8828
    91
\printindex
wenzelm@7046
    92
wenzelm@7046
    93
\end{document}