src/Tools/isac/Doc/isabellesym.sty
changeset 60188 422186a35be8
parent 60187 751b8a13c271
child 60189 6b021e8cb8da
     1.1 --- a/src/Tools/isac/Doc/isabellesym.sty	Thu Apr 08 13:09:44 2021 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,417 +0,0 @@
     1.4 -%%
     1.5 -%% definitions of standard Isabelle symbols
     1.6 -%%
     1.7 -
     1.8 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
     1.9 -\newcommand{\isasymone}{\isamath{\mathbf{1}}}  %requires amssymb
    1.10 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}  %requires amssymb
    1.11 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}}  %requires amssymb
    1.12 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
    1.13 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
    1.14 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}}  %requires amssymb
    1.15 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}}  %requires amssymb
    1.16 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}}  %requires amssymb
    1.17 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
    1.18 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
    1.19 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
    1.20 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
    1.21 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
    1.22 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
    1.23 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
    1.24 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
    1.25 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
    1.26 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
    1.27 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
    1.28 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
    1.29 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
    1.30 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
    1.31 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
    1.32 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
    1.33 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
    1.34 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
    1.35 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
    1.36 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
    1.37 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
    1.38 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
    1.39 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
    1.40 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
    1.41 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
    1.42 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
    1.43 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
    1.44 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
    1.45 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
    1.46 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
    1.47 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
    1.48 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
    1.49 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
    1.50 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
    1.51 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
    1.52 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
    1.53 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
    1.54 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
    1.55 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
    1.56 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
    1.57 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
    1.58 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
    1.59 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
    1.60 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
    1.61 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
    1.62 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
    1.63 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
    1.64 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
    1.65 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
    1.66 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
    1.67 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
    1.68 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
    1.69 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
    1.70 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
    1.71 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
    1.72 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
    1.73 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
    1.74 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
    1.75 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
    1.76 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
    1.77 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
    1.78 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
    1.79 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
    1.80 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
    1.81 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
    1.82 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
    1.83 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
    1.84 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
    1.85 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
    1.86 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
    1.87 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
    1.88 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
    1.89 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
    1.90 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
    1.91 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
    1.92 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
    1.93 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
    1.94 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
    1.95 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
    1.96 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
    1.97 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
    1.98 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
    1.99 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
   1.100 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
   1.101 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
   1.102 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
   1.103 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
   1.104 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
   1.105 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
   1.106 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
   1.107 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
   1.108 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
   1.109 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
   1.110 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
   1.111 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
   1.112 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
   1.113 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
   1.114 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
   1.115 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
   1.116 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
   1.117 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
   1.118 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
   1.119 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
   1.120 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
   1.121 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
   1.122 -\newcommand{\isasymalpha}{\isamath{\alpha}}
   1.123 -\newcommand{\isasymbeta}{\isamath{\beta}}
   1.124 -\newcommand{\isasymgamma}{\isamath{\gamma}}
   1.125 -\newcommand{\isasymdelta}{\isamath{\delta}}
   1.126 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
   1.127 -\newcommand{\isasymzeta}{\isamath{\zeta}}
   1.128 -\newcommand{\isasymeta}{\isamath{\eta}}
   1.129 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
   1.130 -\newcommand{\isasymiota}{\isamath{\iota}}
   1.131 -\newcommand{\isasymkappa}{\isamath{\kappa}}
   1.132 -\newcommand{\isasymlambda}{\isamath{\lambda}}
   1.133 -\newcommand{\isasymmu}{\isamath{\mu}}
   1.134 -\newcommand{\isasymnu}{\isamath{\nu}}
   1.135 -\newcommand{\isasymxi}{\isamath{\xi}}
   1.136 -\newcommand{\isasympi}{\isamath{\pi}}
   1.137 -\newcommand{\isasymrho}{\isamath{\varrho}}
   1.138 -\newcommand{\isasymsigma}{\isamath{\sigma}}
   1.139 -\newcommand{\isasymtau}{\isamath{\tau}}
   1.140 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
   1.141 -\newcommand{\isasymphi}{\isamath{\varphi}}
   1.142 -\newcommand{\isasymchi}{\isamath{\chi}}
   1.143 -\newcommand{\isasympsi}{\isamath{\psi}}
   1.144 -\newcommand{\isasymomega}{\isamath{\omega}}
   1.145 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
   1.146 -\newcommand{\isasymDelta}{\isamath{\Delta}}
   1.147 -\newcommand{\isasymTheta}{\isamath{\Theta}}
   1.148 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
   1.149 -\newcommand{\isasymXi}{\isamath{\Xi}}
   1.150 -\newcommand{\isasymPi}{\isamath{\Pi}}
   1.151 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
   1.152 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
   1.153 -\newcommand{\isasymPhi}{\isamath{\Phi}}
   1.154 -\newcommand{\isasymPsi}{\isamath{\Psi}}
   1.155 -\newcommand{\isasymOmega}{\isamath{\Omega}}
   1.156 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
   1.157 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
   1.158 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
   1.159 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
   1.160 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
   1.161 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
   1.162 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
   1.163 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
   1.164 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
   1.165 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
   1.166 -\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}}  %requires amsmath
   1.167 -\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}}  %requires amsmath
   1.168 -\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}}  %requires amsmath
   1.169 -\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}}  %requires amsmath
   1.170 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
   1.171 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
   1.172 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
   1.173 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
   1.174 -\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}}  %requires amssymb
   1.175 -\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}}  %requires amssymb
   1.176 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
   1.177 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
   1.178 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
   1.179 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
   1.180 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
   1.181 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
   1.182 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
   1.183 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
   1.184 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
   1.185 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
   1.186 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
   1.187 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
   1.188 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
   1.189 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
   1.190 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
   1.191 -\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
   1.192 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
   1.193 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
   1.194 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
   1.195 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
   1.196 -\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
   1.197 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
   1.198 -\newcommand{\isasymup}{\isamath{\uparrow}}
   1.199 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
   1.200 -\newcommand{\isasymdown}{\isamath{\downarrow}}
   1.201 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
   1.202 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
   1.203 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
   1.204 -\newcommand{\isasymlangle}{\isamath{\langle}}
   1.205 -\newcommand{\isasymrangle}{\isamath{\rangle}}
   1.206 -\newcommand{\isasymlceil}{\isamath{\lceil}}
   1.207 -\newcommand{\isasymrceil}{\isamath{\rceil}}
   1.208 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
   1.209 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
   1.210 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
   1.211 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
   1.212 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
   1.213 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
   1.214 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
   1.215 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
   1.216 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
   1.217 -\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
   1.218 -\newcommand{\isasymbottom}{\isamath{\bot}}
   1.219 -\newcommand{\isasymtop}{\isamath{\top}}
   1.220 -\newcommand{\isasymand}{\isamath{\wedge}}
   1.221 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
   1.222 -\newcommand{\isasymor}{\isamath{\vee}}
   1.223 -\newcommand{\isasymOr}{\isamath{\bigvee}}
   1.224 -\newcommand{\isasymforall}{\isamath{\forall\,}}
   1.225 -\newcommand{\isasymexists}{\isamath{\exists\,}}
   1.226 -\newcommand{\isasymnot}{\isamath{\neg}}
   1.227 -\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
   1.228 -\newcommand{\isasymcircle}{\isamath{\ocircle}}  %requires wasysym
   1.229 -\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
   1.230 -\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
   1.231 -\newcommand{\isasymdiamondop}{\isamath{\diamond}}
   1.232 -\newcommand{\isasymsurd}{\isamath{\surd}}
   1.233 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
   1.234 -\newcommand{\isasymTurnstile}{\isamath{\models}}
   1.235 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
   1.236 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
   1.237 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
   1.238 -\newcommand{\isasymle}{\isamath{\le}}
   1.239 -\newcommand{\isasymge}{\isamath{\ge}}
   1.240 -\newcommand{\isasymlless}{\isamath{\ll}}
   1.241 -\newcommand{\isasymggreater}{\isamath{\gg}}
   1.242 -\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
   1.243 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
   1.244 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
   1.245 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
   1.246 -\newcommand{\isasymin}{\isamath{\in}}
   1.247 -\newcommand{\isasymnotin}{\isamath{\notin}}
   1.248 -\newcommand{\isasymsubset}{\isamath{\subset}}
   1.249 -\newcommand{\isasymsupset}{\isamath{\supset}}
   1.250 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
   1.251 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
   1.252 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
   1.253 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
   1.254 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
   1.255 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
   1.256 -\newcommand{\isasyminter}{\isamath{\cap}}
   1.257 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
   1.258 -\newcommand{\isasymunion}{\isamath{\cup}}
   1.259 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
   1.260 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
   1.261 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
   1.262 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
   1.263 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
   1.264 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
   1.265 -\newcommand{\isasympropto}{\isamath{\propto}}
   1.266 -\newcommand{\isasymuplus}{\isamath{\uplus}}
   1.267 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
   1.268 -\newcommand{\isasymnoteq}{\isamath{\not=}}
   1.269 -\newcommand{\isasymsim}{\isamath{\sim}}
   1.270 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
   1.271 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
   1.272 -\newcommand{\isasymapprox}{\isamath{\approx}}
   1.273 -\newcommand{\isasymasymp}{\isamath{\asymp}}
   1.274 -\newcommand{\isasymcong}{\isamath{\cong}}
   1.275 -\newcommand{\isasymsmile}{\isamath{\smile}}
   1.276 -\newcommand{\isasymequiv}{\isamath{\equiv}}
   1.277 -\newcommand{\isasymfrown}{\isamath{\frown}}
   1.278 -\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
   1.279 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
   1.280 -\newcommand{\isasymprec}{\isamath{\prec}}
   1.281 -\newcommand{\isasymsucc}{\isamath{\succ}}
   1.282 -\newcommand{\isasympreceq}{\isamath{\preceq}}
   1.283 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
   1.284 -\newcommand{\isasymparallel}{\isamath{\parallel}}
   1.285 -\newcommand{\isasymbar}{\isamath{\mid}}
   1.286 -\newcommand{\isasymplusminus}{\isamath{\pm}}
   1.287 -\newcommand{\isasymminusplus}{\isamath{\mp}}
   1.288 -\newcommand{\isasymtimes}{\isamath{\times}}
   1.289 -\newcommand{\isasymdiv}{\isamath{\div}}
   1.290 -\newcommand{\isasymcdot}{\isamath{\cdot}}
   1.291 -\newcommand{\isasymstar}{\isamath{\star}}
   1.292 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
   1.293 -\newcommand{\isasymcirc}{\isamath{\circ}}
   1.294 -\newcommand{\isasymdagger}{\isamath{\dagger}}
   1.295 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
   1.296 -\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
   1.297 -\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
   1.298 -\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
   1.299 -\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
   1.300 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
   1.301 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
   1.302 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
   1.303 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
   1.304 -\newcommand{\isasymoplus}{\isamath{\oplus}}
   1.305 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
   1.306 -\newcommand{\isasymotimes}{\isamath{\otimes}}
   1.307 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
   1.308 -\newcommand{\isasymodot}{\isamath{\odot}}
   1.309 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
   1.310 -\newcommand{\isasymominus}{\isamath{\ominus}}
   1.311 -\newcommand{\isasymoslash}{\isamath{\oslash}}
   1.312 -\newcommand{\isasymdots}{\isamath{\dots}}
   1.313 -\newcommand{\isasymcdots}{\isamath{\cdots}}
   1.314 -\newcommand{\isasymSum}{\isamath{\sum\,}}
   1.315 -\newcommand{\isasymProd}{\isamath{\prod\,}}
   1.316 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
   1.317 -\newcommand{\isasyminfinity}{\isamath{\infty}}
   1.318 -\newcommand{\isasymintegral}{\isamath{\int\,}}
   1.319 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
   1.320 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
   1.321 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
   1.322 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
   1.323 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
   1.324 -\newcommand{\isasymaleph}{\isamath{\aleph}}
   1.325 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
   1.326 -\newcommand{\isasymnabla}{\isamath{\nabla}}
   1.327 -\newcommand{\isasympartial}{\isamath{\partial}}
   1.328 -\newcommand{\isasymRe}{\isamath{\Re}}
   1.329 -\newcommand{\isasymIm}{\isamath{\Im}}
   1.330 -\newcommand{\isasymflat}{\isamath{\flat}}
   1.331 -\newcommand{\isasymnatural}{\isamath{\natural}}
   1.332 -\newcommand{\isasymsharp}{\isamath{\sharp}}
   1.333 -\newcommand{\isasymangle}{\isamath{\angle}}
   1.334 -\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}
   1.335 -\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}
   1.336 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
   1.337 -\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}}  %requires textcomp
   1.338 -\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}}  %requires textcomp
   1.339 -\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}}  %requires textcomp
   1.340 -\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}
   1.341 -\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}
   1.342 -\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}
   1.343 -\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}
   1.344 -\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}
   1.345 -\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}
   1.346 -\newcommand{\isasymeuro}{\isatext{\euro}}  %requires eurosym
   1.347 -\newcommand{\isasympounds}{\isamath{\pounds}}
   1.348 -\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
   1.349 -\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
   1.350 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
   1.351 -\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}}  %requires textcomp
   1.352 -\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}
   1.353 -\newcommand{\isasymamalg}{\isamath{\amalg}}
   1.354 -\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
   1.355 -\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
   1.356 -\newcommand{\isasymwp}{\isamath{\wp}}
   1.357 -\newcommand{\isasymwrong}{\isamath{\wr}}
   1.358 -\newcommand{\isasymacute}{\isatext{\'\relax}}
   1.359 -\newcommand{\isasymindex}{\isatext{\i}}
   1.360 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
   1.361 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
   1.362 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
   1.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
   1.364 -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
   1.365 -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
   1.366 -\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
   1.367 -\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
   1.368 -\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
   1.369 -\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
   1.370 -\newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
   1.371 -\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
   1.372 -
   1.373 -\newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont
   1.374 -\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
   1.375 -\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
   1.376 -\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
   1.377 -\newcommand{\isactrlclass}{\isakeywordcontrol{class}}
   1.378 -\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
   1.379 -\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
   1.380 -\newcommand{\isactrlconst}{\isakeywordcontrol{const}}
   1.381 -\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
   1.382 -\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
   1.383 -\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}
   1.384 -\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}
   1.385 -\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}
   1.386 -\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}
   1.387 -\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}
   1.388 -\newcommand{\isactrldir}{\isakeywordcontrol{dir}}
   1.389 -\newcommand{\isactrlfile}{\isakeywordcontrol{file}}
   1.390 -\newcommand{\isactrlhere}{\isakeywordcontrol{here}}
   1.391 -\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
   1.392 -\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
   1.393 -\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
   1.394 -\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
   1.395 -\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
   1.396 -\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
   1.397 -\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
   1.398 -\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
   1.399 -\newcommand{\isactrlpath}{\isakeywordcontrol{path}}
   1.400 -\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
   1.401 -\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
   1.402 -\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
   1.403 -\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
   1.404 -\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
   1.405 -\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
   1.406 -\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
   1.407 -\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
   1.408 -\newcommand{\isactrlterm}{\isakeywordcontrol{term}}
   1.409 -\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}
   1.410 -\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}
   1.411 -\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}
   1.412 -\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}
   1.413 -\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
   1.414 -\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
   1.415 -\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
   1.416 -
   1.417 -\newcommand{\isactrlcode}{\isakeywordcontrol{code}}
   1.418 -\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
   1.419 -\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
   1.420 -\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}