1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Doc/isabellesym.sty Wed Mar 11 15:25:52 2020 +0100
1.3 @@ -0,0 +1,417 @@
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}}