recover original definitions of \isactrlsub etc.;
authorwenzelm
Mon Aug 29 10:28:17 2005 +0200 (2005-08-29)
changeset 171805fefe658a6f8
parent 17179 28802c8a9816
child 17181 5f42dd5e6570
recover original definitions of \isactrlsub etc.;
lib/texinputs/isabelle.sty
     1.1 --- a/lib/texinputs/isabelle.sty	Mon Aug 29 08:34:24 2005 +0200
     1.2 +++ b/lib/texinputs/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4  \newcommand{\isamath}[1]{\emph{$#1$}}
     1.5  \newcommand{\isatext}[1]{\emph{#1}}
     1.6  \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     1.7 -\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
     1.8 -\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
     1.9 -\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
    1.10 -\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
    1.11 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    1.12 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    1.13 +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    1.14 +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    1.15  \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
    1.16  \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
    1.17  \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
    1.18 @@ -89,6 +89,8 @@
    1.19  \chardef\isacharbar=`\|
    1.20  \chardef\isacharbraceright=`\}
    1.21  \chardef\isachartilde=`\~
    1.22 +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
    1.23 +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
    1.24  
    1.25  
    1.26  % keyword and section markup
    1.27 @@ -165,6 +167,8 @@
    1.28  \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
    1.29  \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
    1.30  \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
    1.31 +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
    1.32 +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
    1.33  }
    1.34  
    1.35  \newcommand{\isabellestylesl}{%