# HG changeset patch
# User wenzelm
# Date 1125304097 -7200
# Node ID 5fefe658a6f8d92b74c7c10a35530cdfc397b35c
# Parent  28802c8a981675ee3f914771585cc153d9ccf8d9
recover original definitions of \isactrlsub etc.;

diff -r 28802c8a9816 -r 5fefe658a6f8 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Mon Aug 29 08:34:24 2005 +0200
+++ b/lib/texinputs/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
@@ -22,10 +22,10 @@
 \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{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%