20 |
20 |
21 %symbol markup -- \emph achieves decent spacing via italic corrections |
21 %symbol markup -- \emph achieves decent spacing via italic corrections |
22 \newcommand{\isamath}[1]{\emph{$#1$}} |
22 \newcommand{\isamath}[1]{\emph{$#1$}} |
23 \newcommand{\isatext}[1]{\emph{#1}} |
23 \newcommand{\isatext}[1]{\emph{#1}} |
24 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
24 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
25 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
25 \newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} |
26 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
26 \newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} |
27 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
27 \newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} |
28 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
28 \newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} |
29 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
29 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
147 \renewcommand{\isacharless}{\isamath{<}}% |
147 \renewcommand{\isacharless}{\isamath{<}}% |
148 \renewcommand{\isacharequal}{\isamath{=}}% |
148 \renewcommand{\isacharequal}{\isamath{=}}% |
149 \renewcommand{\isachargreater}{\isamath{>}}% |
149 \renewcommand{\isachargreater}{\isamath{>}}% |
150 \renewcommand{\isacharat}{\isamath{@}}% |
150 \renewcommand{\isacharat}{\isamath{@}}% |
151 \renewcommand{\isacharbrackleft}{\isamath{[}}% |
151 \renewcommand{\isacharbrackleft}{\isamath{[}}% |
|
152 \renewcommand{\isacharbackslash}{\isamath{\backslash}}% |
152 \renewcommand{\isacharbrackright}{\isamath{]}}% |
153 \renewcommand{\isacharbrackright}{\isamath{]}}% |
153 \renewcommand{\isacharunderscore}{\mbox{-}}% |
154 \renewcommand{\isacharunderscore}{\mbox{-}}% |
154 \renewcommand{\isacharbraceleft}{\isamath{\{}}% |
155 \renewcommand{\isacharbraceleft}{\isamath{\{}}% |
155 \renewcommand{\isacharbar}{\isamath{\mid}}% |
156 \renewcommand{\isacharbar}{\isamath{\mid}}% |
156 \renewcommand{\isacharbraceright}{\isamath{\}}}% |
157 \renewcommand{\isacharbraceright}{\isamath{\}}}% |
161 \isabellestyleit% |
162 \isabellestyleit% |
162 \renewcommand{\isastyle}{\small\sl}% |
163 \renewcommand{\isastyle}{\small\sl}% |
163 \renewcommand{\isastyleminor}{\sl}% |
164 \renewcommand{\isastyleminor}{\sl}% |
164 \renewcommand{\isastylescript}{\footnotesize\sl}% |
165 \renewcommand{\isastylescript}{\footnotesize\sl}% |
165 } |
166 } |
|
167 |
|
168 |
|
169 % tagged regions |
|
170 |
|
171 %plain TeX version of comment package -- much faster! |
|
172 \let\isafmtname\fmtname\def\fmtname{plain} |
|
173 \usepackage{comment} |
|
174 \let\fmtname\isafmtname |
|
175 |
|
176 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
|
177 |
|
178 \newcommand{\isakeeptag}[1]% |
|
179 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
180 \newcommand{\isadroptag}[1]% |
|
181 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
182 \newcommand{\isafoldtag}[1]% |
|
183 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} |
|
184 |
|
185 \isakeeptag{theory} |
|
186 \isakeeptag{proof} |
|
187 \isakeeptag{ML} |
|
188 \isakeeptag{visible} |
|
189 \isadroptag{invisible} |
|
190 |
|
191 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |