doc-src/AxClass/generated/isabelle.sty
changeset 10223 31346d22bb54
parent 10207 c7c64cd26fc9
child 10267 325ead6d9457
--- a/doc-src/AxClass/generated/isabelle.sty	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty	Sun Oct 15 19:51:56 2000 +0200
@@ -14,10 +14,18 @@
 
 \newcommand{\isastyle}{\small\tt\slshape}
 \newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
 \newcommand{\isastyletext}{\normalsize\rm}
 \newcommand{\isastyletxt}{\rm}
 \newcommand{\isastylecmt}{\rm}
 
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}_{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}^{#1}$}}
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
@@ -99,43 +107,46 @@
 \newcommand{\isabellestylett}{%
 \renewcommand{\isastyle}{\small\tt}%
 \renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
 }
 \newcommand{\isabellestyleit}{%
 \renewcommand{\isastyle}{\small\it}%
 \renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbang}{\emph{$!$}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
 \renewcommand{\isachardoublequote}{}%
-\renewcommand{\isacharhash}{\emph{$\#$}}%
-\renewcommand{\isachardollar}{\emph{$\$$}}%
-\renewcommand{\isacharpercent}{\emph{$\%$}}%
-\renewcommand{\isacharampersand}{\emph{$\&$}}%
-\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
-\renewcommand{\isacharparenleft}{\emph{$($}}%
-\renewcommand{\isacharparenright}{\emph{$)$}}%
-\renewcommand{\isacharasterisk}{\emph{$*$}}%
-\renewcommand{\isacharplus}{\emph{$+$}}%
-\renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
-\renewcommand{\isacharminus}{\emph{$-$}}%
-\renewcommand{\isachardot}{\emph{$\mathord.$}}%
-\renewcommand{\isacharslash}{\emph{$/$}}%
-\renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
-\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
-\renewcommand{\isacharless}{\emph{$<$}}%
-\renewcommand{\isacharequal}{\emph{$=$}}%
-\renewcommand{\isachargreater}{\emph{$>$}}%
-\renewcommand{\isacharat}{\emph{$@$}}%
-\renewcommand{\isacharbrackleft}{\emph{$[$}}%
-\renewcommand{\isacharbrackright}{\emph{$]$}}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
 \renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
-\renewcommand{\isacharbar}{\emph{$\mid$}}%
-\renewcommand{\isacharbraceright}{\emph{$\}$}}%
-\renewcommand{\isachartilde}{\emph{${}^\sim$}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}^\sim}}%
 }
 
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
 \renewcommand{\isastyle}{\small\sl}%
 \renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
 }