doc-src/ZF/isabelle.sty
changeset 17126 ff9ad5b17100
parent 16353 94e565ded526
child 17175 1eced27ee0e1
equal deleted inserted replaced
17125:e6a82d1a1829 17126:ff9ad5b17100
    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}}{}