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