diff -r 11aa41ed306d -r 1eced27ee0e1 doc-src/AxClass/Group/document/isabelle.sty
--- a/doc-src/AxClass/Group/document/isabelle.sty	Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/AxClass/Group/document/isabelle.sty	Sun Aug 28 19:42:19 2005 +0200
@@ -3,7 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
-%% $Id$
+%% 
 
 %%% Simple document preparation (based on theory token language and symbols)
 
@@ -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}{%