36 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript} |
36 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript} |
37 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} |
37 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} |
38 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript} |
38 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript} |
39 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} |
39 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} |
40 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
40 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
|
41 |
|
42 %blackboard-bold (requires font txmia from pxfonts) |
|
43 \DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it} |
|
44 \SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it} |
|
45 \DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129} |
|
46 \DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130} |
|
47 \DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131} |
|
48 \DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132} |
|
49 \DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133} |
|
50 \DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134} |
|
51 \DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135} |
|
52 \DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136} |
|
53 \DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137} |
|
54 \DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138} |
|
55 \DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139} |
|
56 \DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140} |
|
57 \DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141} |
|
58 \DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142} |
|
59 \DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143} |
|
60 \DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144} |
|
61 \DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145} |
|
62 \DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146} |
|
63 \DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147} |
|
64 \DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148} |
|
65 \DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149} |
|
66 \DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150} |
|
67 \DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151} |
|
68 \DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152} |
|
69 \DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153} |
|
70 \DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154} |
41 |
71 |
42 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} |
72 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} |
43 |
73 |
44 \newdimen\isa@parindent\newdimen\isa@parskip |
74 \newdimen\isa@parindent\newdimen\isa@parskip |
45 |
75 |
110 \chardef\isacharbar=`\|% |
140 \chardef\isacharbar=`\|% |
111 \chardef\isacharbraceright=`\}% |
141 \chardef\isacharbraceright=`\}% |
112 \chardef\isachartilde=`\~% |
142 \chardef\isachartilde=`\~% |
113 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% |
143 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% |
114 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% |
144 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% |
115 \def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
145 \def\isacartoucheopen{\isatext{\guilsinglleft}}% |
116 \def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
146 \def\isacartoucheclose{\isatext{\guilsinglright}}% |
117 } |
147 } |
118 |
148 |
119 |
149 |
120 % keyword and section markup |
150 % keyword and section markup |
121 |
151 |
139 \newcommand{\isaendpar}{\par\medskip} |
169 \newcommand{\isaendpar}{\par\medskip} |
140 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
170 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
141 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} |
171 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} |
142 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} |
172 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} |
143 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
173 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
|
174 |
|
175 |
|
176 % index entries |
|
177 |
|
178 \newcommand{\isaindexdef}[1]{\textbf{#1}} |
|
179 \newcommand{\isaindexref}[1]{#1} |
144 |
180 |
145 |
181 |
146 % styles |
182 % styles |
147 |
183 |
148 \def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
184 \def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
203 \def\isacharunderscore{\mbox{-}}% |
239 \def\isacharunderscore{\mbox{-}}% |
204 \def\isacharbraceleft{\isamath{\{}}% |
240 \def\isacharbraceleft{\isamath{\{}}% |
205 \def\isacharbar{\isamath{\mid}}% |
241 \def\isacharbar{\isamath{\mid}}% |
206 \def\isacharbraceright{\isamath{\}}}% |
242 \def\isacharbraceright{\isamath{\}}}% |
207 \def\isachartilde{\isamath{{}\sp{\sim}}}% |
243 \def\isachartilde{\isamath{{}\sp{\sim}}}% |
208 \def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
244 \def\isacharbackquoteopen{\isatext{\guilsinglleft}}% |
209 \def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
245 \def\isacharbackquoteclose{\isatext{\guilsinglright}}% |
210 } |
246 } |
211 |
247 |
212 \newcommand{\isabellestyleliteral}{% |
248 \newcommand{\isabellestyleliteral}{% |
213 \isabellestyleit% |
249 \isabellestyleit% |
214 \def\isacharunderscore{\_}% |
250 \def\isacharunderscore{\_}% |
237 |
273 |
238 \usepackage[normalem]{ulem} |
274 \usepackage[normalem]{ulem} |
239 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}} |
275 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}} |
240 |
276 |
241 |
277 |
242 % tagged regions |
278 % tags |
243 |
|
244 %plain TeX version of comment package -- much faster! |
|
245 \let\isafmtname\fmtname\def\fmtname{plain} |
|
246 \usepackage{comment} |
|
247 \let\fmtname\isafmtname |
|
248 |
279 |
249 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
280 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
250 |
281 |
251 \newcommand{\isakeeptag}[1]% |
|
252 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
253 \newcommand{\isadroptag}[1]% |
|
254 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
255 \newcommand{\isafoldtag}[1]% |
|
256 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} |
|
257 |
|
258 \isakeeptag{document} |
|
259 \isakeeptag{theory} |
|
260 \isakeeptag{proof} |
|
261 \isakeeptag{ML} |
|
262 \isakeeptag{visible} |
|
263 \isadroptag{invisible} |
|
264 \isakeeptag{important} |
|
265 \isakeeptag{unimportant} |
|
266 |
|
267 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |
282 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |