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