1 % tutorial.sty : Isabelle Tutorial Page Layout |
|
2 % |
|
3 \typeout{Document Style tutorial. Released 9 July 2001} |
|
4 |
|
5 \hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly} |
|
6 \hyphenation{data-type data-types co-data-type co-data-types } |
|
7 |
|
8 %usage: \iflabelundefined{LABEL}{if not defined}{if defined} |
|
9 \newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}} |
|
10 |
|
11 |
|
12 %%%INDEXING use isa-index to process the index |
|
13 |
|
14 \newcommand\seealso[2]{\emph{see also} #1} |
|
15 \usepackage{makeidx} |
|
16 |
|
17 %index, putting page numbers of definitions in boldface |
|
18 \def\bold#1{\textbf{#1}} |
|
19 \newcommand\fnote[1]{#1n} |
|
20 \newcommand\indexbold[1]{\index{#1|bold}} |
|
21 |
|
22 % The alternative to \protect\isa in the indexing macros is |
|
23 % \noexpand\noexpand \noexpand\isa |
|
24 % need TWO levels of \noexpand to delay the expansion of \isa: |
|
25 % the \noexpand\noexpand will leave one \noexpand, to be given to the |
|
26 % (still unexpanded) \isa token. See TeX by Topic, page 122. |
|
27 |
|
28 %%%% for indexing constants, symbols, theorems, ... |
|
29 \newcommand\cdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (constant)}} |
|
30 \newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}} |
|
31 \newcommand\sdxpos[2]{\isa{#1}\index{#2@\protect\isa{#1} (symbol)}} |
|
32 |
|
33 \newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}} |
|
34 \newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}} |
|
35 |
|
36 \newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}} |
|
37 \newcommand\tydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type)}} |
|
38 \newcommand\tcdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type class)}} |
|
39 \newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}} |
|
40 |
|
41 \newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}} |
|
42 \newcommand\cmmdx[1]{\index{#1@\protect\isacommand{#1} (command)}} |
|
43 \newcommand\commdx[1]{\isacommand{#1}\index{#1@\protect\isacommand{#1} (command)}} |
|
44 \newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}} |
|
45 \newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}} |
|
46 \newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}} |
|
47 \newcommand\pgdx[1]{\pgmenu{#1}\index{#1@\protect\pgmenu{#1} (Proof General)}} |
|
48 |
|
49 %set argument in \bf font and index in ROMAN font (for definitions in text!) |
|
50 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@} |
|
51 |
|
52 \newcommand\rmindex[1]{{#1}\index{#1}\@} |
|
53 \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@} |
|
54 \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@} |
|
55 |
|
56 \newcommand{\isadxpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}}\@} |
|
57 \newcommand{\isadxboldpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}|bold}\@} |
|
58 |
|
59 %Commented-out the original versions to see what the index looks like without them. |
|
60 % In any event, they need to use \isa or \protect\isa rather than \texttt. |
|
61 %%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@} |
|
62 %%\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@} |
|
63 \newcommand{\indexboldpos}[2]{#1\@} |
|
64 \newcommand{\ttindexboldpos}[2]{\isa{#1}\@} |
|
65 |
|
66 %\newtheorem{theorem}{Theorem}[section] |
|
67 \newtheorem{Exercise}{Exercise}[section] |
|
68 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} |
|
69 \newcommand{\ttlbr}{\texttt{[|}} |
|
70 \newcommand{\ttrbr}{\texttt{|]}} |
|
71 \newcommand{\ttor}{\texttt{|}} |
|
72 \newcommand{\ttall}{\texttt{!}} |
|
73 \newcommand{\ttuniquex}{\texttt{?!}} |
|
74 \newcommand{\ttEXU}{\texttt{EX!}} |
|
75 \newcommand{\ttAnd}{\texttt{!!}} |
|
76 |
|
77 \newcommand{\isasymignore}{} |
|
78 \newcommand{\isasymimp}{\isasymlongrightarrow} |
|
79 \newcommand{\isasymImp}{\isasymLongrightarrow} |
|
80 \newcommand{\isasymFun}{\isasymRightarrow} |
|
81 \newcommand{\isasymuniqex}{\isamath{\exists!\,}} |
|
82 \renewcommand{\S}{Sect.\ts} |
|
83 |
|
84 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} |
|
85 |
|
86 \newif\ifremarks |
|
87 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi} |
|
88 |
|
89 %names of Isabelle rules |
|
90 \newcommand{\rulename}[1]{\hfill(#1)} |
|
91 \newcommand{\rulenamedx}[1]{\hfill(#1\index{#1@\protect\isa{#1} (theorem)|bold})} |
|
92 |
|
93 %%%% meta-logical connectives |
|
94 |
|
95 \let\Forall=\bigwedge |
|
96 \let\Imp=\Longrightarrow |
|
97 \let\To=\Rightarrow |
|
98 \newcommand{\Var}[1]{{?\!#1}} |
|
99 |
|
100 %%% underscores as ordinary characters, not for subscripting |
|
101 %% use @ or \sb for subscripting; use \at for @ |
|
102 %% only works in \tt font |
|
103 %% must not make _ an active char; would make \ttindex fail! |
|
104 \gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other} |
|
105 \gdef\underscoreon{\catcode`\_=8\makeatother} |
|
106 \chardef\other=12 |
|
107 \chardef\at=`\@ |
|
108 |
|
109 % alternative underscore |
|
110 \def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em} |
|
111 |
|
112 |
|
113 %%%% ``WARNING'' environment: 2 ! characters separated by negative thin space |
|
114 \def\warnbang{\vtop to 0pt{\vss\hbox{\Huge\bf!\!!}\vss}} |
|
115 \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
116 \small %%WAS\baselineskip=0.9\baselineskip |
|
117 \noindent \hangindent\parindent \hangafter=-2 |
|
118 \hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces}% |
|
119 {\par\endgroup\medbreak} |
|
120 |
|
121 %%%% ``PROOF GENERAL'' environment |
|
122 \def\pghead{\lower3pt\vbox to 0pt{\vss\hbox{\includegraphics[width=12pt]{pghead}}\vss}} |
|
123 \newenvironment{pgnote}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
124 \small \noindent \hangindent\parindent \hangafter=-2 |
|
125 \hbox to0pt{\hskip-\hangindent \pghead\hfill}\ignorespaces}% |
|
126 {\par\endgroup\medbreak} |
|
127 \newcommand{\pgmenu}[1]{\textsf{#1}} |
|
128 |
|
129 |
|
130 %%%% Standard logical symbols |
|
131 \let\turn=\vdash |
|
132 \let\conj=\wedge |
|
133 \let\disj=\vee |
|
134 \let\imp=\rightarrow |
|
135 \let\bimp=\leftrightarrow |
|
136 \newcommand\all[1]{\forall#1.} %quantification |
|
137 \newcommand\ex[1]{\exists#1.} |
|
138 \newcommand{\pair}[1]{\langle#1\rangle} |
|
139 |
|
140 \newcommand{\lparr}{\mathopen{(\!|}} |
|
141 \newcommand{\rparr}{\mathclose{|\!)}} |
|
142 \newcommand{\fs}{\mathpunct{,\,}} |
|
143 \newcommand{\ty}{\mathrel{::}} |
|
144 \newcommand{\asn}{\mathrel{:=}} |
|
145 \newcommand{\more}{\ldots} |
|
146 \newcommand{\record}[1]{\lparr #1 \rparr} |
|
147 \newcommand{\dtt}{\mathord.} |
|
148 |
|
149 \newcommand\lbrakk{\mathopen{[\![}} |
|
150 \newcommand\rbrakk{\mathclose{]\!]}} |
|
151 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
|
152 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
|
153 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
|
154 \newcommand{\Text}[1]{\mbox{#1}} |
|
155 |
|
156 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} |
|
157 \newcommand{\dsh}{\mathit{\dshsym}} |
|
158 |
|
159 \let\int=\cap |
|
160 \let\un=\cup |
|
161 \let\inter=\bigcap |
|
162 \let\union=\bigcup |
|
163 |
|
164 \def\ML{{\sc ml}} |
|
165 \def\AST{{\sc ast}} |
|
166 |
|
167 %macros to change the treatment of symbols |
|
168 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
|
169 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
|
170 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
|
171 |
|
172 %redefinition of \sloppy and \fussy to use \emergencystretch |
|
173 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} |
|
174 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} |
|
175 |
|
176 %non-bf version of description |
|
177 \def\descrlabel#1{\hspace\labelsep #1} |
|
178 \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}} |
|
179 \let\enddescr\endlist |
|
180 |
|
181 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
|
182 % generate text italic rather than math italic by default. This makes |
|
183 % multi-letter identifiers look better. The mathcode for character c |
|
184 % is set to |"7000| (variable family) + |"400| (text italic) + |c|. |
|
185 % |
|
186 \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% |
|
187 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 |
|
188 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 |
|
189 \advance\count0 by1 \advance\count1 by1 \repeat}} |
|
190 \@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} |
|
191 \@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} |
|