# HG changeset patch # User wenzelm # Date 971906287 -7200 # Node ID 325ead6d945795024a4b2d830b42407c4e3a4190 # Parent 41f6be79b44f6d1b28ca8f8ad235e9ec108a3d52 updated; diff -r 41f6be79b44f -r 325ead6d9457 doc-src/AxClass/generated/isabelle.sty --- a/doc-src/AxClass/generated/isabelle.sty Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/AxClass/generated/isabelle.sty Wed Oct 18 23:58:07 2000 +0200 @@ -23,8 +23,8 @@ \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}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newdimen\isa@parindent\newdimen\isa@parskip @@ -141,7 +141,7 @@ \renewcommand{\isacharbraceleft}{\isamath{\{}}% \renewcommand{\isacharbar}{\isamath{\mid}}% \renewcommand{\isacharbraceright}{\isamath{\}}}% -\renewcommand{\isachartilde}{\isamath{{}^\sim}}% +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% } \newcommand{\isabellestylesl}{% diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/CTL/document/CTLind.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Oct 18 23:58:07 2000 +0200 @@ -0,0 +1,134 @@ +% +\begin{isabellebody}% +\def\isabellecontext{CTLind}% +% +\isamarkupsubsection{CTL revisited} +% +\begin{isamarkuptext}% +\label{sec:CTL-revisited} +In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a +model checker for CTL. In particular the proof of the +\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as +simple as one might intuitively expect, due to the \isa{SOME} operator +involved. The purpose of this section is to show how an inductive definition +can help to simplify the proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}. + +Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does +not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says +that if no infinite path from some state \isa{s} is \isa{A}-avoiding, +then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set +\isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path: +% Second proof of opposite direction, directly by well-founded induction +% on the initial segment of M that avoids A.% +\end{isamarkuptext}% +\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline +\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline +\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}% +\begin{isamarkuptext}% +It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} +with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path +starting with \isa{s} because (by definition of \isa{Avoid}) there is a +finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}. +The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However, +this requires the following +reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; +the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.% +\end{isamarkuptext}% +\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline +\ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +\noindent +The base case (\isa{t\ {\isacharequal}\ s}) is trivial (\isa{blast}). +In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} +starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate +the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with +\isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term +expresses. That fact that this is a path starting with \isa{t} and that +the instantiated induction hypothesis implies the conclusion is shown by +simplification. + +Now we come to the key lemma. It says that if \isa{t} can be reached by a +finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, +provided there is no infinite \isa{A}-avoiding path starting from \isa{s}.% +\end{isamarkuptext}% +\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% +\begin{isamarkuptxt}% +\noindent +The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as already the base +case would be a problem, but to proceed by well-founded induction \isa{t}. Hence \isa{t\ {\isasymin}\ Avoid\ s\ A} needs to be brought into the conclusion as +well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below). +But induction with respect to which well-founded relation? The restriction +of \isa{M} to \isa{Avoid\ s\ A}: +\begin{isabelle}% +\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% +\end{isabelle} +As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths +starting from \isa{s} implies well-foundedness of this relation. For the +moment we assume this and proceed with the induction:% +\end{isamarkuptxt}% +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline +\ \ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +Now can assume additionally (induction hypothesis) that if \isa{t\ {\isasymnotin}\ A} +then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now +we have to prove that \isa{t} is in \isa{A} or all successors of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. If \isa{t} is not in \isa{A}, the second +\isa{Avoid}-rule implies that all successors of \isa{t} are in +\isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and +hence, by the induction hypothesis, all successors of \isa{t} are indeed in +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:% +\end{isamarkuptxt}% +\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}% +\begin{isamarkuptxt}% +Having proved the main goal we return to the proof obligation that the above +relation is indeed well-founded. This is proved by contraposition: we assume +the relation is not well-founded. Thus there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem +\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: +\begin{isabelle}% +\ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}% +\end{isabelle} +From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite +\isa{A}-avoiding path starting in \isa{s} follows, just as required for +the contraposition.% +\end{isamarkuptxt}% +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means +that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned +into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is, +\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now +\begin{isabelle}% +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}% +\end{isabelle} +The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, +in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true +by the first \isa{Avoid}-rule). Isabelle confirms this:% +\end{isamarkuptext}% +\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline +\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{Tree2}% +\def\isabellecontext{Tree{\isadigit{2}}}% % \begin{isamarkuptext}% \noindent In Exercise~\ref{ex:Tree} we defined a function diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Misc/document/arith1.tex --- a/doc-src/TutorialI/Misc/document/arith1.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith1.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{arith1}% +\def\isabellecontext{arith{\isadigit{1}}}% \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline \end{isabellebody}% %%% Local Variables: diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Misc/document/arith2.tex --- a/doc-src/TutorialI/Misc/document/arith2.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith2.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{arith2}% +\def\isabellecontext{arith{\isadigit{2}}}% \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline \end{isabellebody}% diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Misc/document/arith3.tex --- a/doc-src/TutorialI/Misc/document/arith3.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{arith3}% +\def\isabellecontext{arith{\isadigit{3}}}% \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline \end{isabellebody}% %%% Local Variables: diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Misc/document/case_exprs.tex --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{case_exprs}% +\def\isabellecontext{case{\isacharunderscore}exprs}% % \isamarkupsubsection{Case expressions} % diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Misc/document/prime_def.tex --- a/doc-src/TutorialI/Misc/document/prime_def.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{prime_def}% +\def\isabellecontext{prime{\isacharunderscore}def}% % \begin{isamarkuptext}% \begin{warn} diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Recdef/document/Nested0.tex --- a/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{Nested0}% +\def\isabellecontext{Nested{\isadigit{0}}}% % \begin{isamarkuptext}% In \S\ref{sec:nested-datatype} we defined the datatype of terms% diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Recdef/document/Nested1.tex --- a/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{Nested1}% +\def\isabellecontext{Nested{\isadigit{1}}}% % \begin{isamarkuptext}% \noindent diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Recdef/document/Nested2.tex --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{Nested2}% +\def\isabellecontext{Nested{\isadigit{2}}}% % \begin{isamarkuptext}% \noindent diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/Trie/document/Option2.tex --- a/doc-src/TutorialI/Trie/document/Option2.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Trie/document/Option2.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{Option2}% +\def\isabellecontext{Option{\isadigit{2}}}% \isanewline \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}% %%% Local Variables: diff -r 41f6be79b44f -r 325ead6d9457 doc-src/TutorialI/isabelle.sty --- a/doc-src/TutorialI/isabelle.sty Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/isabelle.sty Wed Oct 18 23:58:07 2000 +0200 @@ -23,8 +23,8 @@ \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}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newdimen\isa@parindent\newdimen\isa@parskip @@ -141,7 +141,7 @@ \renewcommand{\isacharbraceleft}{\isamath{\{}}% \renewcommand{\isacharbar}{\isamath{\mid}}% \renewcommand{\isacharbraceright}{\isamath{\}}}% -\renewcommand{\isachartilde}{\isamath{{}^\sim}}% +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% } \newcommand{\isabellestylesl}{%