doc-src/IsarRef/isar-ref.tex
author blanchet
Wed Mar 04 11:05:29 2009 +0100 (2009-03-04 ago)
changeset 30242 aea5d7fa7ef5
parent 30240 5b25fee0362c
parent 30185 6889bfc03804
child 30569 696f93184f0d
permissions -rw-r--r--
Merge.
wenzelm@7836
     1
\documentclass[12pt,a4paper,fleqn]{report}
wenzelm@28838
     2
\usepackage{amssymb}
wenzelm@28838
     3
\usepackage[greek,english]{babel}
wenzelm@28838
     4
\usepackage[latin1]{inputenc}
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@26906
    12
\usepackage{../isabelle,../isabellesym}
wenzelm@26738
    13
\usepackage{../ttbox,,../rail,../railsetup}
wenzelm@28773
    14
\usepackage{supertabular}
wenzelm@26738
    15
\usepackage{style}
wenzelm@26738
    16
\usepackage{../pdfsetup}
wenzelm@7046
    17
wenzelm@26741
    18
\hyphenation{Isabelle}
wenzelm@26741
    19
\hyphenation{Isar}
wenzelm@26741
    20
wenzelm@26741
    21
\isadroptag{theory}
wenzelm@7046
    22
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
wenzelm@26870
    23
\author{\emph{Makarius Wenzel} \\[3ex]
wenzelm@26870
    24
  With Contributions by
wenzelm@26870
    25
  Clemens Ballarin,
wenzelm@26870
    26
  Stefan Berghofer, \\
wenzelm@30185
    27
  Timothy Bourke
wenzelm@27038
    28
  Lucas Dixon,
wenzelm@30185
    29
  Florian Haftmann, \\
wenzelm@30185
    30
  Gerwin Klein,
wenzelm@27038
    31
  Alexander Krauss,
wenzelm@30185
    32
  Tobias Nipkow, \\
wenzelm@30185
    33
  David von Oheimb,
wenzelm@27038
    34
  Larry Paulson,
wenzelm@26870
    35
  and Sebastian Skalberg
wenzelm@26870
    36
}
wenzelm@7046
    37
wenzelm@7050
    38
\makeindex
wenzelm@7050
    39
wenzelm@9204
    40
\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
wenzelm@7167
    41
\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
wenzelm@8596
    42
\railterm{name,nameref,text,type,term,prop,atom}
wenzelm@7134
    43
wenzelm@13048
    44
\railalias{ident}{\railtok{ident}}
wenzelm@13048
    45
\railalias{longident}{\railtok{longident}}
wenzelm@13048
    46
\railalias{symident}{\railtok{symident}}
wenzelm@13048
    47
\railalias{var}{\railtok{var}}
wenzelm@13048
    48
\railalias{textvar}{\railtok{textvar}}
wenzelm@13048
    49
\railalias{typefree}{\railtok{typefree}}
wenzelm@13048
    50
\railalias{typevar}{\railtok{typevar}}
wenzelm@13048
    51
\railalias{nat}{\railtok{nat}}
wenzelm@13048
    52
\railalias{string}{\railtok{string}}
wenzelm@13048
    53
\railalias{verbatim}{\railtok{verbatim}}
wenzelm@13048
    54
\railalias{keyword}{\railtok{keyword}}
wenzelm@8594
    55
wenzelm@13048
    56
\railalias{name}{\railqtok{name}}
wenzelm@13048
    57
\railalias{nameref}{\railqtok{nameref}}
wenzelm@13048
    58
\railalias{text}{\railqtok{text}}
wenzelm@13048
    59
\railalias{type}{\railqtok{type}}
wenzelm@13048
    60
\railalias{term}{\railqtok{term}}
wenzelm@13048
    61
\railalias{prop}{\railqtok{prop}}
wenzelm@13048
    62
\railalias{atom}{\railqtok{atom}}
wenzelm@7134
    63
wenzelm@26786
    64
\railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}
wenzelm@26786
    65
\railalias{equiv}{\isasymequiv}\railterm{equiv}
wenzelm@26786
    66
\railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}
wenzelm@26786
    67
\railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}
wenzelm@26786
    68
\railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}
wenzelm@26848
    69
\railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}
wenzelm@26848
    70
\railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}
wenzelm@26848
    71
wenzelm@26786
    72
wenzelm@18021
    73
\chardef\charbackquote=`\`
wenzelm@18021
    74
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
wenzelm@18021
    75
wenzelm@7046
    76
wenzelm@7046
    77
\begin{document}
wenzelm@7046
    78
wenzelm@7046
    79
\maketitle 
wenzelm@7046
    80
wenzelm@7046
    81
\pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@7046
    82
wenzelm@29718
    83
\part{Basic Concepts}
wenzelm@27035
    84
\input{Thy/document/Introduction.tex}
wenzelm@29716
    85
\input{Thy/document/Framework.tex}
wenzelm@29730
    86
\input{Thy/document/First_Order_Logic.tex}
wenzelm@29718
    87
\part{General Language Elements}
wenzelm@27037
    88
\input{Thy/document/Outer_Syntax.tex}
wenzelm@28751
    89
\input{Thy/document/Document_Preparation.tex}
wenzelm@26869
    90
\input{Thy/document/Spec.tex}
wenzelm@26869
    91
\input{Thy/document/Proof.tex}
wenzelm@28762
    92
\input{Thy/document/Inner_Syntax.tex}
wenzelm@27048
    93
\input{Thy/document/Misc.tex}
wenzelm@26782
    94
\input{Thy/document/Generic.tex}
wenzelm@29718
    95
\part{Object-Logics}
wenzelm@26840
    96
\input{Thy/document/HOL_Specific.tex}
wenzelm@26840
    97
\input{Thy/document/HOLCF_Specific.tex}
wenzelm@26840
    98
\input{Thy/document/ZF_Specific.tex}
wenzelm@7046
    99
wenzelm@29718
   100
\part{Appendix}
wenzelm@7895
   101
\appendix
wenzelm@26779
   102
\input{Thy/document/Quick_Reference.tex}
wenzelm@28838
   103
\let\int\intorig
wenzelm@28838
   104
\input{Thy/document/Symbols.tex}
wenzelm@26846
   105
\input{Thy/document/ML_Tactic.tex}
wenzelm@7895
   106
wenzelm@7046
   107
\begingroup
wenzelm@30116
   108
  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
wenzelm@7046
   109
  \bibliography{../manual}
wenzelm@7046
   110
\endgroup
wenzelm@7046
   111
wenzelm@8828
   112
\printindex
wenzelm@7046
   113
wenzelm@7046
   114
\end{document}