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