1 |
1 |
2 %% $Id$ |
2 %% $Id$ |
3 |
3 |
4 \documentclass[12pt]{report} |
4 \documentclass[12pt,fleqn]{report} |
5 \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../isar,../pdfsetup} |
5 \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup} |
6 |
6 |
7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} |
7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} |
8 \author{\emph{Markus Wenzel} \\ TU M\"unchen} |
8 \author{\emph{Markus Wenzel} \\ TU M\"unchen} |
9 |
9 |
10 \makeindex |
10 \makeindex |
|
11 |
|
12 \railterm{lbrace,rbrace,llbrace,rrbrace} |
|
13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim} |
|
14 |
|
15 \railalias{name}{\railqtoken{name}} |
|
16 \railalias{nameref}{\railqtoken{nameref}} |
|
17 \railalias{text}{\railqtoken{text}} |
|
18 \railalias{type}{\railqtoken{type}} |
|
19 \railalias{term}{\railqtoken{term}} |
|
20 \railalias{prop}{\railqtoken{prop}} |
|
21 \railalias{atom}{\railqtoken{atom}} |
11 |
22 |
12 |
23 |
13 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
24 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
14 |
25 |
15 \pagestyle{headings} |
26 \pagestyle{headings} |
16 \sloppy |
27 \sloppy |
17 \binperiod %%%treat . like a binary operator |
28 \binperiod %%%treat . like a binary operator |
18 |
29 |
19 \railalias{lbrace}{\ttlbrace} |
30 \renewcommand{\phi}{\varphi} |
20 \railalias{rbrace}{\ttrbrace} |
|
21 \railterm{lbrace,rbrace} |
|
22 |
31 |
23 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim} |
|
24 \railterm{name,nameref,text,type,term,prop,atom} |
|
25 |
|
26 \makeatletter |
|
27 \newcommand{\railtoken}[1]{{\rail@termfont{#1}}} |
|
28 \newcommand{\railnonterm}[1]{{\rail@nontfont{#1}}} |
|
29 \makeatother |
|
30 |
|
31 \newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}} |
|
32 \newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}} |
|
33 |
32 |
34 \begin{document} |
33 \begin{document} |
35 |
34 |
36 \underscoreoff |
35 \underscoreoff |
37 |
36 |