doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Mon Oct 16 13:21:01 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Oct 16 20:33:15 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}%
}