--- a/lib/texinputs/isabelle.sty Fri Oct 13 18:32:08 2000 +0200
+++ b/lib/texinputs/isabelle.sty Sun Oct 15 19:50:35 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}%
}