--- a/doc-src/ZF/isabelle.sty Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/ZF/isabelle.sty Sun Aug 28 19:42:19 2005 +0200
@@ -31,6 +31,7 @@
\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
\newdimen\isa@parindent\newdimen\isa@parskip
@@ -49,11 +50,13 @@
\newcommand{\isaindent}[1]{\hphantom{#1}}
\newcommand{\isanewline}{\mbox{}\par\mbox{}}
-\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
+\newcommand{\isasep}{}
\newcommand{\isadigit}[1]{#1}
\chardef\isacharbang=`\!
\chardef\isachardoublequote=`\"
+\chardef\isachardoublequoteopen=`\"
+\chardef\isachardoublequoteclose=`\"
\chardef\isacharhash=`\#
\chardef\isachardollar=`\$
\chardef\isacharpercent=`\%
@@ -80,6 +83,8 @@
\chardef\isacharcircum=`\^
\chardef\isacharunderscore=`\_
\chardef\isacharbackquote=`\`
+\chardef\isacharbackquoteopen=`\`
+\chardef\isacharbackquoteclose=`\`
\chardef\isacharbraceleft=`\{
\chardef\isacharbar=`\|
\chardef\isacharbraceright=`\}
@@ -129,6 +134,8 @@
\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
\renewcommand{\isacharbang}{\isamath{!}}%
\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isachardoublequoteopen}{}%
+\renewcommand{\isachardoublequoteclose}{}%
\renewcommand{\isacharhash}{\isamath{\#}}%
\renewcommand{\isachardollar}{\isamath{\$}}%
\renewcommand{\isacharpercent}{\isamath{\%}}%
@@ -156,6 +163,8 @@
\renewcommand{\isacharbar}{\isamath{\mid}}%
\renewcommand{\isacharbraceright}{\isamath{\}}}%
\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
+\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
+\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
}
\newcommand{\isabellestylesl}{%