%%

%% definitions of standard Isabelle symbols

%%

\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb

\newcommand{\isasymone}{\isamath{\mathbf{1}}}  %requires amssymb

\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}  %requires amssymb

\newcommand{\isasymthree}{\isamath{\mathbf{3}}}  %requires amssymb

\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb

\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb

\newcommand{\isasymsix}{\isamath{\mathbf{6}}}  %requires amssymb

\newcommand{\isasymseven}{\isamath{\mathbf{7}}}  %requires amssymb

\newcommand{\isasymeight}{\isamath{\mathbf{8}}}  %requires amssymb

\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb

\newcommand{\isasymA}{\isamath{\mathcal{A}}}

\newcommand{\isasymB}{\isamath{\mathcal{B}}}

\newcommand{\isasymC}{\isamath{\mathcal{C}}}

\newcommand{\isasymD}{\isamath{\mathcal{D}}}

\newcommand{\isasymE}{\isamath{\mathcal{E}}}

\newcommand{\isasymF}{\isamath{\mathcal{F}}}

\newcommand{\isasymG}{\isamath{\mathcal{G}}}

\newcommand{\isasymH}{\isamath{\mathcal{H}}}

\newcommand{\isasymI}{\isamath{\mathcal{I}}}

\newcommand{\isasymJ}{\isamath{\mathcal{J}}}

\newcommand{\isasymK}{\isamath{\mathcal{K}}}

\newcommand{\isasymL}{\isamath{\mathcal{L}}}

\newcommand{\isasymM}{\isamath{\mathcal{M}}}

\newcommand{\isasymN}{\isamath{\mathcal{N}}}

\newcommand{\isasymO}{\isamath{\mathcal{O}}}

\newcommand{\isasymP}{\isamath{\mathcal{P}}}

\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}

\newcommand{\isasymR}{\isamath{\mathcal{R}}}

\newcommand{\isasymS}{\isamath{\mathcal{S}}}

\newcommand{\isasymT}{\isamath{\mathcal{T}}}

\newcommand{\isasymU}{\isamath{\mathcal{U}}}

\newcommand{\isasymV}{\isamath{\mathcal{V}}}

\newcommand{\isasymW}{\isamath{\mathcal{W}}}

\newcommand{\isasymX}{\isamath{\mathcal{X}}}

\newcommand{\isasymY}{\isamath{\mathcal{Y}}}

\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}

\newcommand{\isasyma}{\isamath{\mathrm{a}}}

\newcommand{\isasymb}{\isamath{\mathrm{b}}}

\newcommand{\isasymc}{\isamath{\mathrm{c}}}

\newcommand{\isasymd}{\isamath{\mathrm{d}}}

\newcommand{\isasyme}{\isamath{\mathrm{e}}}

\newcommand{\isasymf}{\isamath{\mathrm{f}}}

\newcommand{\isasymg}{\isamath{\mathrm{g}}}

\newcommand{\isasymh}{\isamath{\mathrm{h}}}

\newcommand{\isasymi}{\isamath{\mathrm{i}}}

\newcommand{\isasymj}{\isamath{\mathrm{j}}}

\newcommand{\isasymk}{\isamath{\mathrm{k}}}

\newcommand{\isasyml}{\isamath{\mathrm{l}}}

\newcommand{\isasymm}{\isamath{\mathrm{m}}}

\newcommand{\isasymn}{\isamath{\mathrm{n}}}

\newcommand{\isasymo}{\isamath{\mathrm{o}}}

\newcommand{\isasymp}{\isamath{\mathrm{p}}}

\newcommand{\isasymq}{\isamath{\mathrm{q}}}

\newcommand{\isasymr}{\isamath{\mathrm{r}}}

\newcommand{\isasyms}{\isamath{\mathrm{s}}}

\newcommand{\isasymt}{\isamath{\mathrm{t}}}

\newcommand{\isasymu}{\isamath{\mathrm{u}}}

\newcommand{\isasymv}{\isamath{\mathrm{v}}}

\newcommand{\isasymw}{\isamath{\mathrm{w}}}

\newcommand{\isasymx}{\isamath{\mathrm{x}}}

\newcommand{\isasymy}{\isamath{\mathrm{y}}}

\newcommand{\isasymz}{\isamath{\mathrm{z}}}

\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak

\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak

\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak

\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak

\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak

\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak

\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak

\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak

\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak

\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak

\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak

\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak

\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak

\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak

\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak

\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak

\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak

\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak

\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak

\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak

\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak

\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak

\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak

\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak

\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak

\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak

\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak

\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak

\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak

\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak

\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak

\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak

\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak

\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak

\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak

\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak

\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak

\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak

\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak

\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak

\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak

\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak

\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak

\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak

\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak

\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak

\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak

\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak

\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak

\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak

\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak

\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak

\newcommand{\isasymalpha}{\isamath{\alpha}}

\newcommand{\isasymbeta}{\isamath{\beta}}

\newcommand{\isasymgamma}{\isamath{\gamma}}

\newcommand{\isasymdelta}{\isamath{\delta}}

\newcommand{\isasymepsilon}{\isamath{\varepsilon}}

\newcommand{\isasymzeta}{\isamath{\zeta}}

\newcommand{\isasymeta}{\isamath{\eta}}

\newcommand{\isasymtheta}{\isamath{\vartheta}}

\newcommand{\isasymiota}{\isamath{\iota}}

\newcommand{\isasymkappa}{\isamath{\kappa}}

\newcommand{\isasymlambda}{\isamath{\lambda}}

\newcommand{\isasymmu}{\isamath{\mu}}

\newcommand{\isasymnu}{\isamath{\nu}}

\newcommand{\isasymxi}{\isamath{\xi}}

\newcommand{\isasympi}{\isamath{\pi}}

\newcommand{\isasymrho}{\isamath{\varrho}}

\newcommand{\isasymsigma}{\isamath{\sigma}}

\newcommand{\isasymtau}{\isamath{\tau}}

\newcommand{\isasymupsilon}{\isamath{\upsilon}}

\newcommand{\isasymphi}{\isamath{\varphi}}

\newcommand{\isasymchi}{\isamath{\chi}}

\newcommand{\isasympsi}{\isamath{\psi}}

\newcommand{\isasymomega}{\isamath{\omega}}

\newcommand{\isasymGamma}{\isamath{\Gamma}}

\newcommand{\isasymDelta}{\isamath{\Delta}}

\newcommand{\isasymTheta}{\isamath{\Theta}}

\newcommand{\isasymLambda}{\isamath{\Lambda}}

\newcommand{\isasymXi}{\isamath{\Xi}}

\newcommand{\isasymPi}{\isamath{\Pi}}

\newcommand{\isasymSigma}{\isamath{\Sigma}}

\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}

\newcommand{\isasymPhi}{\isamath{\Phi}}

\newcommand{\isasymPsi}{\isamath{\Psi}}

\newcommand{\isasymOmega}{\isamath{\Omega}}

\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}

\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}

\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}

\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}

\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}

\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}

\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}

\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}

\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}

\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}

\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}}  %requires amsmath

\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}}  %requires amsmath

\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}}  %requires amsmath

\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}}  %requires amsmath

\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}

\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}

\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}

\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}

\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}}  %requires amssymb

\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}}  %requires amssymb

\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}

\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}

\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}

\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}

\newcommand{\isasymmapsto}{\isamath{\mapsto}}

\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}

\newcommand{\isasymmidarrow}{\isamath{\relbar}}

\newcommand{\isasymMidarrow}{\isamath{\Relbar}}

\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}

\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}

\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}

\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}

\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}

\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}

\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}

\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb

\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb

\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb

\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb

\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb

\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb

\newcommand{\isasymColon}{\isamath{\mathrel{::}}}

\newcommand{\isasymup}{\isamath{\uparrow}}

\newcommand{\isasymUp}{\isamath{\Uparrow}}

\newcommand{\isasymdown}{\isamath{\downarrow}}

\newcommand{\isasymDown}{\isamath{\Downarrow}}

\newcommand{\isasymupdown}{\isamath{\updownarrow}}

\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}

\newcommand{\isasymlangle}{\isamath{\langle}}

\newcommand{\isasymrangle}{\isamath{\rangle}}

\newcommand{\isasymlceil}{\isamath{\lceil}}

\newcommand{\isasymrceil}{\isamath{\rceil}}

\newcommand{\isasymlfloor}{\isamath{\lfloor}}

\newcommand{\isasymrfloor}{\isamath{\rfloor}}

\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}

\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}

\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}

\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}

\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}

\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}

\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel

\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel

\newcommand{\isasymbottom}{\isamath{\bot}}

\newcommand{\isasymtop}{\isamath{\top}}

\newcommand{\isasymand}{\isamath{\wedge}}

\newcommand{\isasymAnd}{\isamath{\bigwedge}}

\newcommand{\isasymor}{\isamath{\vee}}

\newcommand{\isasymOr}{\isamath{\bigvee}}

\newcommand{\isasymforall}{\isamath{\forall\,}}

\newcommand{\isasymexists}{\isamath{\exists\,}}

\newcommand{\isasymnot}{\isamath{\neg}}

\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb

\newcommand{\isasymcircle}{\isamath{\ocircle}}  %requires wasysym

\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb

\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb

\newcommand{\isasymdiamondop}{\isamath{\diamond}}

\newcommand{\isasymsurd}{\isamath{\surd}}

\newcommand{\isasymturnstile}{\isamath{\vdash}}

\newcommand{\isasymTurnstile}{\isamath{\models}}

\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}

\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}

\newcommand{\isasymstileturn}{\isamath{\dashv}}

\newcommand{\isasymle}{\isamath{\le}}

\newcommand{\isasymge}{\isamath{\ge}}

\newcommand{\isasymlless}{\isamath{\ll}}

\newcommand{\isasymggreater}{\isamath{\gg}}

\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb

\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb

\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb

\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb

\newcommand{\isasymin}{\isamath{\in}}

\newcommand{\isasymnotin}{\isamath{\notin}}

\newcommand{\isasymsubset}{\isamath{\subset}}

\newcommand{\isasymsupset}{\isamath{\supset}}

\newcommand{\isasymsubseteq}{\isamath{\subseteq}}

\newcommand{\isasymsupseteq}{\isamath{\supseteq}}

\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb

\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb

\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}

\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}

\newcommand{\isasyminter}{\isamath{\cap}}

\newcommand{\isasymInter}{\isamath{\bigcap\,}}

\newcommand{\isasymunion}{\isamath{\cup}}

\newcommand{\isasymUnion}{\isamath{\bigcup\,}}

\newcommand{\isasymsqunion}{\isamath{\sqcup}}

\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}

\newcommand{\isasymsqinter}{\isamath{\sqcap}}

\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd

\newcommand{\isasymsetminus}{\isamath{\setminus}}

\newcommand{\isasympropto}{\isamath{\propto}}

\newcommand{\isasymuplus}{\isamath{\uplus}}

\newcommand{\isasymUplus}{\isamath{\biguplus\,}}

\newcommand{\isasymnoteq}{\isamath{\not=}}

\newcommand{\isasymsim}{\isamath{\sim}}

\newcommand{\isasymdoteq}{\isamath{\doteq}}

\newcommand{\isasymsimeq}{\isamath{\simeq}}

\newcommand{\isasymapprox}{\isamath{\approx}}

\newcommand{\isasymasymp}{\isamath{\asymp}}

\newcommand{\isasymcong}{\isamath{\cong}}

\newcommand{\isasymsmile}{\isamath{\smile}}

\newcommand{\isasymequiv}{\isamath{\equiv}}

\newcommand{\isasymfrown}{\isamath{\frown}}

\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb

\newcommand{\isasymbowtie}{\isamath{\bowtie}}

\newcommand{\isasymprec}{\isamath{\prec}}

\newcommand{\isasymsucc}{\isamath{\succ}}

\newcommand{\isasympreceq}{\isamath{\preceq}}

\newcommand{\isasymsucceq}{\isamath{\succeq}}

\newcommand{\isasymparallel}{\isamath{\parallel}}

\newcommand{\isasymbar}{\isamath{\mid}}

\newcommand{\isasymplusminus}{\isamath{\pm}}

\newcommand{\isasymminusplus}{\isamath{\mp}}

\newcommand{\isasymtimes}{\isamath{\times}}

\newcommand{\isasymdiv}{\isamath{\div}}

\newcommand{\isasymcdot}{\isamath{\cdot}}

\newcommand{\isasymstar}{\isamath{\star}}

\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}

\newcommand{\isasymcirc}{\isamath{\circ}}

\newcommand{\isasymdagger}{\isamath{\dagger}}

\newcommand{\isasymddagger}{\isamath{\ddagger}}

\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb

\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb

\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb

\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb

\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}

\newcommand{\isasymtriangleright}{\isamath{\triangleright}}

\newcommand{\isasymtriangle}{\isamath{\triangle}}

\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb

\newcommand{\isasymoplus}{\isamath{\oplus}}

\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}

\newcommand{\isasymotimes}{\isamath{\otimes}}

\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}

\newcommand{\isasymodot}{\isamath{\odot}}

\newcommand{\isasymOdot}{\isamath{\bigodot\,}}

\newcommand{\isasymominus}{\isamath{\ominus}}

\newcommand{\isasymoslash}{\isamath{\oslash}}

\newcommand{\isasymdots}{\isamath{\dots}}

\newcommand{\isasymcdots}{\isamath{\cdots}}

\newcommand{\isasymSum}{\isamath{\sum\,}}

\newcommand{\isasymProd}{\isamath{\prod\,}}

\newcommand{\isasymCoprod}{\isamath{\coprod\,}}

\newcommand{\isasyminfinity}{\isamath{\infty}}

\newcommand{\isasymintegral}{\isamath{\int\,}}

\newcommand{\isasymointegral}{\isamath{\oint\,}}

\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}

\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}

\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}

\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}

\newcommand{\isasymaleph}{\isamath{\aleph}}

\newcommand{\isasymemptyset}{\isamath{\emptyset}}

\newcommand{\isasymnabla}{\isamath{\nabla}}

\newcommand{\isasympartial}{\isamath{\partial}}

\newcommand{\isasymRe}{\isamath{\Re}}

\newcommand{\isasymIm}{\isamath{\Im}}

\newcommand{\isasymflat}{\isamath{\flat}}

\newcommand{\isasymnatural}{\isamath{\natural}}

\newcommand{\isasymsharp}{\isamath{\sharp}}

\newcommand{\isasymangle}{\isamath{\angle}}

\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}

\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}

\newcommand{\isasyminverse}{\isamath{{}^{-1}}}

\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}}  %requires textcomp

\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}}  %requires textcomp

\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}}  %requires textcomp

\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}

\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}

\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}

\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}

\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}

\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}

\newcommand{\isasymeuro}{\isatext{\euro}}  %requires eurosym

\newcommand{\isasympounds}{\isamath{\pounds}}

\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb

\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp

\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp

\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}}  %requires textcomp

\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}

\newcommand{\isasymamalg}{\isamath{\amalg}}

\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb

\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb

\newcommand{\isasymwp}{\isamath{\wp}}

\newcommand{\isasymwrong}{\isamath{\wr}}

\newcommand{\isasymacute}{\isatext{\'\relax}}

\newcommand{\isasymindex}{\isatext{\i}}

\newcommand{\isasymdieresis}{\isatext{\"\relax}}

\newcommand{\isasymcedilla}{\isatext{\c\relax}}

\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}

\newcommand{\isasymsome}{\isamath{\epsilon\,}}

\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}

\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}

\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}

\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}

\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym

\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}

\newcommand{\isasymcomment}{\isatext{\isastylecmt---}}

\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}

\newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont

\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}

\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}

\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}

\newcommand{\isactrlclass}{\isakeywordcontrol{class}}

\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}

\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}

\newcommand{\isactrlconst}{\isakeywordcontrol{const}}

\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}

\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}

\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}

\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}

\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}

\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}

\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}

\newcommand{\isactrldir}{\isakeywordcontrol{dir}}

\newcommand{\isactrlfile}{\isakeywordcontrol{file}}

\newcommand{\isactrlhere}{\isakeywordcontrol{here}}

\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}

\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}

\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}

\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}

\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}

\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}

\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}

\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}

\newcommand{\isactrlpath}{\isakeywordcontrol{path}}

\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}

\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}

\newcommand{\isactrlprint}{\isakeywordcontrol{print}}

\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}

\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}

\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}

\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}

\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}

\newcommand{\isactrlterm}{\isakeywordcontrol{term}}

\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}

\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}

\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}

\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}

\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}

\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}

\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}

\newcommand{\isactrlcode}{\isakeywordcontrol{code}}

\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}

\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}

\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}