updated;
authorwenzelm
Thu Oct 12 18:09:06 2000 +0200 (2000-10-12)
changeset 102111bece7f35762
parent 10210 e8aa81362f41
child 10212 33fe2d701ddd
updated;
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/isabelle.sty
doc-src/TutorialI/isabellesym.sty
     1.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 12 18:06:31 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 12 18:09:06 2000 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  by simplification and clarification%
     1.5  \end{isamarkuptxt}%
     1.6  \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
     1.7 -\isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
     1.8 +\isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
     1.9  \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
    1.10  \begin{isamarkuptxt}%
    1.11  \noindent
    1.12 @@ -120,7 +120,7 @@
    1.13  \begin{isamarkuptext}%
    1.14  \noindent
    1.15  is proved by a variant of contraposition (\isa{swap}:
    1.16 -\isa{{\isasymlbrakk}{\isasymnot}\ Pa{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Pa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
    1.17 +\isa{{\isasymlbrakk}{\isasymnot}\ Q{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
    1.18  and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
    1.19  simplifying with the definition of \isa{af} finishes the proof.
    1.20  
     2.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:06:31 2000 +0200
     2.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:09:06 2000 +0200
     2.3 @@ -101,7 +101,7 @@
     2.4  \end{isabelle}
     2.5  which is proved by \isa{lfp}-induction:%
     2.6  \end{isamarkuptxt}%
     2.7 -\ \isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharparenright}\isanewline
     2.8 +\ \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline
     2.9  \ \ \isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline
    2.10  \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
    2.11  \begin{isamarkuptxt}%
     3.1 --- a/doc-src/TutorialI/isabelle.sty	Thu Oct 12 18:06:31 2000 +0200
     3.2 +++ b/doc-src/TutorialI/isabelle.sty	Thu Oct 12 18:09:06 2000 +0200
     3.3 @@ -98,7 +98,7 @@
     3.4  
     3.5  \newcommand{\isabellestylett}{%
     3.6  \renewcommand{\isastyle}{\small\tt}%
     3.7 -\renewcommand{\isastyleminor}{\tt}%
     3.8 +\renewcommand{\isastyleminor}{\small\tt}%
     3.9  }
    3.10  \newcommand{\isabellestyleit}{%
    3.11  \renewcommand{\isastyle}{\small\it}%
     4.1 --- a/doc-src/TutorialI/isabellesym.sty	Thu Oct 12 18:06:31 2000 +0200
     4.2 +++ b/doc-src/TutorialI/isabellesym.sty	Thu Oct 12 18:09:06 2000 +0200
     4.3 @@ -18,219 +18,225 @@
     4.4  % automatically inserts italic corrections around symbols wherever
     4.5  % appropriate.
     4.6  
     4.7 -\newcommand{\isasymspacespace}{~~}
     4.8 -\newcommand{\isasymGamma}{$\Gamma$}
     4.9 -\newcommand{\isasymDelta}{$\Delta$}
    4.10 -\newcommand{\isasymTheta}{$\Theta$}
    4.11 -\newcommand{\isasymLambda}{$\Lambda$}
    4.12 -\newcommand{\isasymXi}{$\Xi$}
    4.13 -\newcommand{\isasymPi}{$\Pi$}
    4.14 -\newcommand{\isasymSigma}{$\Sigma$}
    4.15 -\newcommand{\isasymUpsilon}{$\Upsilon$}
    4.16 -\newcommand{\isasymPhi}{$\Phi$}
    4.17 -\newcommand{\isasymPsi}{$\Psi$}
    4.18 -\newcommand{\isasymOmega}{$\Omega$}
    4.19 -\newcommand{\isasymalpha}{$\alpha$}
    4.20 -\newcommand{\isasymbeta}{$\beta$}
    4.21 -\newcommand{\isasymgamma}{$\gamma$}
    4.22 -\newcommand{\isasymdelta}{$\delta$}
    4.23 -\newcommand{\isasymepsilon}{$\varepsilon$}
    4.24 -\newcommand{\isasymzeta}{$\zeta$}
    4.25 -\newcommand{\isasymeta}{$\eta$}
    4.26 -\newcommand{\isasymtheta}{$\vartheta$}
    4.27 -\newcommand{\isasymiota}{$\iota$}
    4.28 -\newcommand{\isasymkappa}{$\kappa$}
    4.29 -\newcommand{\isasymlambda}{$\lambda$}
    4.30 -\newcommand{\isasymmu}{$\mu$}
    4.31 -\newcommand{\isasymnu}{$\nu$}
    4.32 -\newcommand{\isasymxi}{$\xi$}
    4.33 -\newcommand{\isasympi}{$\pi$}
    4.34 -\newcommand{\isasymrho}{$\varrho$}
    4.35 -\newcommand{\isasymsigma}{$\sigma$}
    4.36 -\newcommand{\isasymtau}{$\tau$}
    4.37 -\newcommand{\isasymupsilon}{$\upsilon$}
    4.38 -\newcommand{\isasymphi}{$\varphi$}
    4.39 -\newcommand{\isasymchi}{$\chi$}
    4.40 -\newcommand{\isasympsi}{$\psi$}
    4.41 -\newcommand{\isasymomega}{$\omega$}
    4.42 -\newcommand{\isasymnot}{\emph{$\neg$}}
    4.43 -\newcommand{\isasymand}{\emph{$\wedge$}}
    4.44 -\newcommand{\isasymor}{\emph{$\vee$}}
    4.45 -\newcommand{\isasymforall}{\emph{$\forall\,$}}
    4.46 -\newcommand{\isasymexists}{\emph{$\exists\,$}}
    4.47 -\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}}
    4.48 -\newcommand{\isasymlceil}{\emph{$\lceil$}}
    4.49 -\newcommand{\isasymrceil}{\emph{$\rceil$}}
    4.50 -\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
    4.51 -\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
    4.52 -\newcommand{\isasymturnstile}{\emph{$\vdash$}}
    4.53 -\newcommand{\isasymTurnstile}{\emph{$\models$}}
    4.54 -\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
    4.55 -\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
    4.56 -\newcommand{\isasymcdot}{\emph{$\cdot$}}
    4.57 -\newcommand{\isasymin}{\emph{$\in$}}
    4.58 -\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
    4.59 -\newcommand{\isasyminter}{\emph{$\cap$}}
    4.60 -\newcommand{\isasymunion}{\emph{$\cup$}}
    4.61 -\newcommand{\isasymInter}{\emph{$\bigcap\,$}}
    4.62 -\newcommand{\isasymUnion}{\emph{$\bigcup\,$}}
    4.63 -\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
    4.64 -\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
    4.65 -\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}}  %requires stmaryrd
    4.66 -\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}}
    4.67 -\newcommand{\isasymbottom}{\emph{$\bot$}}
    4.68 -\newcommand{\isasymdoteq}{\emph{$\doteq$}}
    4.69 -\newcommand{\isasymequiv}{\emph{$\equiv$}}
    4.70 -\newcommand{\isasymnoteq}{\emph{$\not=$}}
    4.71 -\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
    4.72 -\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
    4.73 -\newcommand{\isasymprec}{\emph{$\prec$}}
    4.74 -\newcommand{\isasympreceq}{\emph{$\preceq$}}
    4.75 -\newcommand{\isasymsucc}{\emph{$\succ$}}
    4.76 -\newcommand{\isasymapprox}{\emph{$\approx$}}
    4.77 -\newcommand{\isasymsim}{\emph{$\sim$}}
    4.78 -\newcommand{\isasymsimeq}{\emph{$\simeq$}}
    4.79 -\newcommand{\isasymle}{\emph{$\le$}}
    4.80 -\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
    4.81 -\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
    4.82 -\newcommand{\isasymmidarrow}{\emph{$\relbar$}}
    4.83 -\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
    4.84 -\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
    4.85 -\newcommand{\isasymMidarrow}{\emph{$\Relbar$}}
    4.86 -\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
    4.87 -\newcommand{\isasymfrown}{\emph{$\frown$}}
    4.88 -\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
    4.89 -\newcommand{\isasymleadsto}{\emph{$\leadsto$}}  %requires latexsym
    4.90 -\newcommand{\isasymup}{\emph{$\uparrow$}}
    4.91 -\newcommand{\isasymdown}{\emph{$\downarrow$}}
    4.92 -\newcommand{\isasymnotin}{\emph{$\notin$}}
    4.93 -\newcommand{\isasymtimes}{\emph{$\times$}}
    4.94 -\newcommand{\isasymoplus}{\emph{$\oplus$}}
    4.95 -\newcommand{\isasymominus}{\emph{$\ominus$}}
    4.96 -\newcommand{\isasymotimes}{\emph{$\otimes$}}
    4.97 -\newcommand{\isasymoslash}{\emph{$\oslash$}}
    4.98 -\newcommand{\isasymsubset}{\emph{$\subset$}}
    4.99 -\newcommand{\isasyminfinity}{\emph{$\infty$}}
   4.100 -\newcommand{\isasymbox}{\emph{$\Box$}}  %requires latexsym
   4.101 -\newcommand{\isasymdiamond}{\emph{$\Diamond$}}  %requires latexsym
   4.102 -\newcommand{\isasymcirc}{\emph{$\circ$}}
   4.103 -\newcommand{\isasymbullet}{\emph{$\bullet$}}
   4.104 -\newcommand{\isasymparallel}{\emph{$\parallel$}}
   4.105 -\newcommand{\isasymsurd}{\emph{$\surd$}}
   4.106 -\newcommand{\isasymcopyright}{\emph{\copyright}}
   4.107 -\newcommand{\isasymplusminus}{\emph{$\pm$}}
   4.108 -\newcommand{\isasymdiv}{\emph{$\div$}}
   4.109 -\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
   4.110 -\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
   4.111 -\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
   4.112 -\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
   4.113 -\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
   4.114 -\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
   4.115 -\newcommand{\isasymbar}{\emph{$\mid$}}
   4.116 -\newcommand{\isasymhyphen}{\emph{\rm-}}
   4.117 -\newcommand{\isasymmacron}{\emph{\rm\=\relax}}
   4.118 -\newcommand{\isasymexclamdown}{\emph{\rm\textexclamdown}}
   4.119 -\newcommand{\isasymquestiondown}{\emph{\rm\textquestiondown}}
   4.120 -\newcommand{\isasymguillemotleft}{\emph{\flqq}}  %requires babel
   4.121 -\newcommand{\isasymguillemotright}{\emph{\frqq}}  %requires babel
   4.122 -\newcommand{\isasymdegree}{\emph{\rm\textdegree}}  %requires latin1
   4.123 -\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}  %requires latin1
   4.124 -\newcommand{\isasymonequarter}{\emph{\rm\textonequarter}}  %requires latin1
   4.125 -\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}  %requires latin1
   4.126 -\newcommand{\isasymonehalf}{\emph{\rm\textonehalf}}  %requires latin1
   4.127 -\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}  %requires latin1
   4.128 -\newcommand{\isasymthreequarters}{\emph{\rm\textthreequarters}}  %requires latin1
   4.129 -\newcommand{\isasymparagraph}{\emph{\P}}
   4.130 -\newcommand{\isasymregistered}{\emph{\rm\textregistered}}
   4.131 -\newcommand{\isasymordfeminine}{\emph{\rm\textordfeminine}}
   4.132 -\newcommand{\isasymordmasculine}{\emph{\rm\textordmasculine}}
   4.133 -\newcommand{\isasymsection}{\emph{\S}}
   4.134 -\newcommand{\isasympounds}{\emph{$\pounds$}}
   4.135 -\newcommand{\isasymyen}{\emph{\yen}}  %requires amssymb
   4.136 -\newcommand{\isasymcent}{\emph{\cent}}  %requires wasysym
   4.137 -\newcommand{\isasymcurrency}{\emph{\currency}}  %requires wasysym
   4.138 -\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}
   4.139 -\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
   4.140 -\newcommand{\isasymtop}{\emph{$\top$}}
   4.141 -\newcommand{\isasymcong}{\emph{$\cong$}}
   4.142 -\newcommand{\isasymclubsuit}{\emph{$\clubsuit$}}
   4.143 -\newcommand{\isasymdiamondsuit}{\emph{$\diamondsuit$}}
   4.144 -\newcommand{\isasymheartsuit}{\emph{$\heartsuit$}}
   4.145 -\newcommand{\isasymspadesuit}{\emph{$\spadesuit$}}
   4.146 -\newcommand{\isasymleftrightarrow}{\emph{$\leftrightarrow$}}
   4.147 -\newcommand{\isasymge}{\emph{$\ge$}}
   4.148 -\newcommand{\isasympropto}{\emph{$\propto$}}
   4.149 -\newcommand{\isasympartial}{\emph{$\partial$}}
   4.150 -\newcommand{\isasymdots}{\emph{$\dots$}}
   4.151 -\newcommand{\isasymaleph}{\emph{$\aleph$}}
   4.152 -\newcommand{\isasymIm}{\emph{$\Im$}}
   4.153 -\newcommand{\isasymRe}{\emph{$\Re$}}
   4.154 -\newcommand{\isasymwp}{\emph{$\wp$}}
   4.155 -\newcommand{\isasymemptyset}{\emph{$\emptyset$}}
   4.156 -\newcommand{\isasymangle}{\emph{$\angle$}}
   4.157 -\newcommand{\isasymnabla}{\emph{$\nabla$}}
   4.158 -\newcommand{\isasymProd}{\emph{$\prod\,$}}
   4.159 -\newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}}
   4.160 -\newcommand{\isasymUparrow}{\emph{$\Uparrow$}}
   4.161 -\newcommand{\isasymDownarrow}{\emph{$\Downarrow$}}
   4.162 -\newcommand{\isasymlozenge}{\emph{$\lozenge$}}  %requires amssym
   4.163 -\newcommand{\isasymlangle}{\emph{$\langle$}}
   4.164 -\newcommand{\isasymrangle}{\emph{$\rangle$}}
   4.165 -\newcommand{\isasymSum}{\emph{$\sum\,$}}
   4.166 -\newcommand{\isasymintegral}{\emph{$\int\,$}}
   4.167 -\newcommand{\isasymdagger}{\emph{$\dagger$}}
   4.168 -\newcommand{\isasymsharp}{\emph{$\sharp$}}
   4.169 -\newcommand{\isasymstar}{\emph{$\star$}}
   4.170 -\newcommand{\isasymtriangleright}{\emph{$\triangleright$}}
   4.171 -\newcommand{\isasymlhd}{\emph{$\lhd$}}
   4.172 -\newcommand{\isasymtriangle}{\emph{$\triangle$}}
   4.173 -\newcommand{\isasymrhd}{\emph{$\rhd$}}
   4.174 -\newcommand{\isasymunlhd}{\emph{$\unlhd$}}
   4.175 -\newcommand{\isasymunrhd}{\emph{$\unrhd$}}
   4.176 -\newcommand{\isasymtriangleleft}{\emph{$\triangleleft$}}
   4.177 -\newcommand{\isasymnatural}{\emph{$\natural$}}
   4.178 -\newcommand{\isasymflat}{\emph{$\flat$}}
   4.179 -\newcommand{\isasymamalg}{\emph{$\amalg$}}
   4.180 -\newcommand{\isasymmho}{\emph{$\mho$}}  %requires latexsym
   4.181 -\newcommand{\isasymupdownarrow}{\emph{$\updownarrow$}}
   4.182 -\newcommand{\isasymlongmapsto}{\emph{$\longmapsto$}}
   4.183 -\newcommand{\isasymUpdownarrow}{\emph{$\Updownarrow$}}
   4.184 -\newcommand{\isasymhookleftarrow}{\emph{$\hookleftarrow$}}
   4.185 -\newcommand{\isasymhookrightarrow}{\emph{$\hookrightarrow$}}
   4.186 -\newcommand{\isasymrightleftharpoons}{\emph{$\rightleftharpoons$}}
   4.187 -\newcommand{\isasymleftharpoondown}{\emph{$\leftharpoondown$}}
   4.188 -\newcommand{\isasymrightharpoondown}{\emph{$\rightharpoondown$}}
   4.189 -\newcommand{\isasymleftharpoonup}{\emph{$\leftharpoonup$}}
   4.190 -\newcommand{\isasymrightharpoonup}{\emph{$\rightharpoonup$}}
   4.191 -\newcommand{\isasymasymp}{\emph{$\asymp$}}
   4.192 -\newcommand{\isasymminusplus}{\emph{$\mp$}}
   4.193 -\newcommand{\isasymbowtie}{\emph{$\bowtie$}}
   4.194 -\newcommand{\isasymcdots}{\emph{$\cdots$}}
   4.195 -\newcommand{\isasymodot}{\emph{$\odot$}}
   4.196 -\newcommand{\isasymsupset}{\emph{$\supset$}}
   4.197 -\newcommand{\isasymsupseteq}{\emph{$\supseteq$}}
   4.198 -\newcommand{\isasymsqsupset}{\emph{$\sqsupset$}}  %requires latexsym
   4.199 -\newcommand{\isasymsqsupseteq}{\emph{$\sqsupseteq$}}
   4.200 -\newcommand{\isasymll}{\emph{$\ll$}}
   4.201 -\newcommand{\isasymgg}{\emph{$\gg$}}
   4.202 -\newcommand{\isasymuplus}{\emph{$\uplus$}}
   4.203 -\newcommand{\isasymsmile}{\emph{$\smile$}}
   4.204 -\newcommand{\isasymsucceq}{\emph{$\succeq$}}
   4.205 -\newcommand{\isasymstileturn}{\emph{$\dashv$}}
   4.206 -\newcommand{\isasymOr}{\emph{$\bigvee$}}
   4.207 -\newcommand{\isasymbiguplus}{\emph{$\biguplus$}}
   4.208 -\newcommand{\isasymddagger}{\emph{$\ddagger$}}
   4.209 -\newcommand{\isasymJoin}{\emph{$\Join$}}  %requires latexsym
   4.210 -\newcommand{\isasymbool}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{B}$}}
   4.211 -\newcommand{\isasymcomplex}{\emph{$\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu$}}
   4.212 -\newcommand{\isasymnat}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{N}$}}
   4.213 -\newcommand{\isasymrat}{\emph{$\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu$}}
   4.214 -\newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}}
   4.215 -\newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}}
   4.216 -\newcommand{\isasymlesssim}{\emph{$\lesssim$}}  %requires amssymb
   4.217 -\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}}  %requires amssymb
   4.218 -\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}}  %requires amssymb
   4.219 -\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}}  %requires amssymb
   4.220 -\newcommand{\isasymtriangleq}{\emph{$\triangleq$}}  %requires amssymb
   4.221 -\newcommand{\isasymlparr}{\emph{$\mathopen{(\mkern-3mu\mid}$}}
   4.222 -\newcommand{\isasymrparr}{\emph{$\mathclose{\mid\mkern-3mu)}$}}
   4.223 +\newcommand{\isamath}[1]{\emph{$#1$}}
   4.224 +\newcommand{\isatext}[1]{\emph{#1}}
   4.225 +
   4.226 +
   4.227 +% symbol definitions
   4.228 +
   4.229 +\newcommand{\isasymspacespace}{\isamath{~~}}
   4.230 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
   4.231 +\newcommand{\isasymDelta}{\isamath{\Delta}}
   4.232 +\newcommand{\isasymTheta}{\isamath{\Theta}}
   4.233 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
   4.234 +\newcommand{\isasymXi}{\isamath{\Xi}}
   4.235 +\newcommand{\isasymPi}{\isamath{\Pi}}
   4.236 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
   4.237 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
   4.238 +\newcommand{\isasymPhi}{\isamath{\Phi}}
   4.239 +\newcommand{\isasymPsi}{\isamath{\Psi}}
   4.240 +\newcommand{\isasymOmega}{\isamath{\Omega}}
   4.241 +\newcommand{\isasymalpha}{\isamath{\alpha}}
   4.242 +\newcommand{\isasymbeta}{\isamath{\beta}}
   4.243 +\newcommand{\isasymgamma}{\isamath{\gamma}}
   4.244 +\newcommand{\isasymdelta}{\isamath{\delta}}
   4.245 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
   4.246 +\newcommand{\isasymzeta}{\isamath{\zeta}}
   4.247 +\newcommand{\isasymeta}{\isamath{\eta}}
   4.248 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
   4.249 +\newcommand{\isasymiota}{\isamath{\iota}}
   4.250 +\newcommand{\isasymkappa}{\isamath{\kappa}}
   4.251 +\newcommand{\isasymlambda}{\isamath{\lambda}}
   4.252 +\newcommand{\isasymmu}{\isamath{\mu}}
   4.253 +\newcommand{\isasymnu}{\isamath{\nu}}
   4.254 +\newcommand{\isasymxi}{\isamath{\xi}}
   4.255 +\newcommand{\isasympi}{\isamath{\pi}}
   4.256 +\newcommand{\isasymrho}{\isamath{\varrho}}
   4.257 +\newcommand{\isasymsigma}{\isamath{\sigma}}
   4.258 +\newcommand{\isasymtau}{\isamath{\tau}}
   4.259 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
   4.260 +\newcommand{\isasymphi}{\isamath{\varphi}}
   4.261 +\newcommand{\isasymchi}{\isamath{\chi}}
   4.262 +\newcommand{\isasympsi}{\isamath{\psi}}
   4.263 +\newcommand{\isasymomega}{\isamath{\omega}}
   4.264 +\newcommand{\isasymnot}{\isamath{\neg}}
   4.265 +\newcommand{\isasymand}{\isamath{\wedge}}
   4.266 +\newcommand{\isasymor}{\isamath{\vee}}
   4.267 +\newcommand{\isasymforall}{\isamath{\forall\,}}
   4.268 +\newcommand{\isasymexists}{\isamath{\exists\,}}
   4.269 +\newcommand{\isasymAnd}{\isamath{\bigwedge\,}}
   4.270 +\newcommand{\isasymlceil}{\isamath{\lceil}}
   4.271 +\newcommand{\isasymrceil}{\isamath{\rceil}}
   4.272 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
   4.273 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
   4.274 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
   4.275 +\newcommand{\isasymTurnstile}{\isamath{\models}}
   4.276 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
   4.277 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
   4.278 +\newcommand{\isasymcdot}{\isamath{\cdot}}
   4.279 +\newcommand{\isasymin}{\isamath{\in}}
   4.280 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
   4.281 +\newcommand{\isasyminter}{\isamath{\cap}}
   4.282 +\newcommand{\isasymunion}{\isamath{\cup}}
   4.283 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
   4.284 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
   4.285 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
   4.286 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
   4.287 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
   4.288 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
   4.289 +\newcommand{\isasymbottom}{\isamath{\bot}}
   4.290 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
   4.291 +\newcommand{\isasymequiv}{\isamath{\equiv}}
   4.292 +\newcommand{\isasymnoteq}{\isamath{\not=}}
   4.293 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
   4.294 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
   4.295 +\newcommand{\isasymprec}{\isamath{\prec}}
   4.296 +\newcommand{\isasympreceq}{\isamath{\preceq}}
   4.297 +\newcommand{\isasymsucc}{\isamath{\succ}}
   4.298 +\newcommand{\isasymapprox}{\isamath{\approx}}
   4.299 +\newcommand{\isasymsim}{\isamath{\sim}}
   4.300 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
   4.301 +\newcommand{\isasymle}{\isamath{\le}}
   4.302 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
   4.303 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
   4.304 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
   4.305 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
   4.306 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
   4.307 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
   4.308 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
   4.309 +\newcommand{\isasymfrown}{\isamath{\frown}}
   4.310 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
   4.311 +\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires latexsym
   4.312 +\newcommand{\isasymup}{\isamath{\uparrow}}
   4.313 +\newcommand{\isasymdown}{\isamath{\downarrow}}
   4.314 +\newcommand{\isasymnotin}{\isamath{\notin}}
   4.315 +\newcommand{\isasymtimes}{\isamath{\times}}
   4.316 +\newcommand{\isasymoplus}{\isamath{\oplus}}
   4.317 +\newcommand{\isasymominus}{\isamath{\ominus}}
   4.318 +\newcommand{\isasymotimes}{\isamath{\otimes}}
   4.319 +\newcommand{\isasymoslash}{\isamath{\oslash}}
   4.320 +\newcommand{\isasymsubset}{\isamath{\subset}}
   4.321 +\newcommand{\isasyminfinity}{\isamath{\infty}}
   4.322 +\newcommand{\isasymbox}{\isamath{\Box}}  %requires latexsym
   4.323 +\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
   4.324 +\newcommand{\isasymcirc}{\isamath{\circ}}
   4.325 +\newcommand{\isasymbullet}{\isamath{\bullet}}
   4.326 +\newcommand{\isasymparallel}{\isamath{\parallel}}
   4.327 +\newcommand{\isasymsurd}{\isamath{\surd}}
   4.328 +\newcommand{\isasymcopyright}{\isatext{\copyright}}
   4.329 +\newcommand{\isasymplusminus}{\isamath{\pm}}
   4.330 +\newcommand{\isasymdiv}{\isamath{\div}}
   4.331 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
   4.332 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
   4.333 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
   4.334 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
   4.335 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
   4.336 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
   4.337 +\newcommand{\isasymbar}{\isamath{\mid}}
   4.338 +\newcommand{\isasymhyphen}{\isatext{\rm-}}
   4.339 +\newcommand{\isasymmacron}{\isatext{\rm\=\relax}}
   4.340 +\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
   4.341 +\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
   4.342 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
   4.343 +\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
   4.344 +\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
   4.345 +\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
   4.346 +\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
   4.347 +\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
   4.348 +\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
   4.349 +\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
   4.350 +\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
   4.351 +\newcommand{\isasymparagraph}{\isatext{\P}}
   4.352 +\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
   4.353 +\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
   4.354 +\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
   4.355 +\newcommand{\isasymsection}{\isatext{\S}}
   4.356 +\newcommand{\isasympounds}{\isamath{\pounds}}
   4.357 +\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
   4.358 +\newcommand{\isasymcent}{\isatext{\cent}}  %requires wasysym
   4.359 +\newcommand{\isasymcurrency}{\isatext{\currency}}  %requires wasysym
   4.360 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
   4.361 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
   4.362 +\newcommand{\isasymtop}{\isamath{\top}}
   4.363 +\newcommand{\isasymcong}{\isamath{\cong}}
   4.364 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
   4.365 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
   4.366 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
   4.367 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
   4.368 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
   4.369 +\newcommand{\isasymge}{\isamath{\ge}}
   4.370 +\newcommand{\isasympropto}{\isamath{\propto}}
   4.371 +\newcommand{\isasympartial}{\isamath{\partial}}
   4.372 +\newcommand{\isasymdots}{\isamath{\dots}}
   4.373 +\newcommand{\isasymaleph}{\isamath{\aleph}}
   4.374 +\newcommand{\isasymIm}{\isamath{\Im}}
   4.375 +\newcommand{\isasymRe}{\isamath{\Re}}
   4.376 +\newcommand{\isasymwp}{\isamath{\wp}}
   4.377 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
   4.378 +\newcommand{\isasymangle}{\isamath{\angle}}
   4.379 +\newcommand{\isasymnabla}{\isamath{\nabla}}
   4.380 +\newcommand{\isasymProd}{\isamath{\prod\,}}
   4.381 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
   4.382 +\newcommand{\isasymUparrow}{\isamath{\Uparrow}}
   4.383 +\newcommand{\isasymDownarrow}{\isamath{\Downarrow}}
   4.384 +\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
   4.385 +\newcommand{\isasymlangle}{\isamath{\langle}}
   4.386 +\newcommand{\isasymrangle}{\isamath{\rangle}}
   4.387 +\newcommand{\isasymSum}{\isamath{\sum\,}}
   4.388 +\newcommand{\isasymintegral}{\isamath{\int\,}}
   4.389 +\newcommand{\isasymdagger}{\isamath{\dagger}}
   4.390 +\newcommand{\isasymsharp}{\isamath{\sharp}}
   4.391 +\newcommand{\isasymstar}{\isamath{\star}}
   4.392 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
   4.393 +\newcommand{\isasymlhd}{\isamath{\lhd}}
   4.394 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
   4.395 +\newcommand{\isasymrhd}{\isamath{\rhd}}
   4.396 +\newcommand{\isasymunlhd}{\isamath{\unlhd}}
   4.397 +\newcommand{\isasymunrhd}{\isamath{\unrhd}}
   4.398 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
   4.399 +\newcommand{\isasymnatural}{\isamath{\natural}}
   4.400 +\newcommand{\isasymflat}{\isamath{\flat}}
   4.401 +\newcommand{\isasymamalg}{\isamath{\amalg}}
   4.402 +\newcommand{\isasymmho}{\isamath{\mho}}  %requires latexsym
   4.403 +\newcommand{\isasymupdownarrow}{\isamath{\updownarrow}}
   4.404 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
   4.405 +\newcommand{\isasymUpdownarrow}{\isamath{\Updownarrow}}
   4.406 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
   4.407 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
   4.408 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
   4.409 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
   4.410 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
   4.411 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
   4.412 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
   4.413 +\newcommand{\isasymasymp}{\isamath{\asymp}}
   4.414 +\newcommand{\isasymminusplus}{\isamath{\mp}}
   4.415 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
   4.416 +\newcommand{\isasymcdots}{\isamath{\cdots}}
   4.417 +\newcommand{\isasymodot}{\isamath{\odot}}
   4.418 +\newcommand{\isasymsupset}{\isamath{\supset}}
   4.419 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
   4.420 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires latexsym
   4.421 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
   4.422 +\newcommand{\isasymll}{\isamath{\ll}}
   4.423 +\newcommand{\isasymgg}{\isamath{\gg}}
   4.424 +\newcommand{\isasymuplus}{\isamath{\uplus}}
   4.425 +\newcommand{\isasymsmile}{\isamath{\smile}}
   4.426 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
   4.427 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
   4.428 +\newcommand{\isasymOr}{\isamath{\bigvee}}
   4.429 +\newcommand{\isasymbiguplus}{\isamath{\biguplus}}
   4.430 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
   4.431 +\newcommand{\isasymJoin}{\isamath{\Join}}  %requires latexsym
   4.432 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
   4.433 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
   4.434 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
   4.435 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
   4.436 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
   4.437 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
   4.438 +\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
   4.439 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
   4.440 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
   4.441 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
   4.442 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
   4.443 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
   4.444 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}