doc-src/AxClass/generated/isabellesym.sty

 %%
 %% Author: Markus Wenzel, TU Muenchen
 %%
 %% definitions of standard Isabelle symbols
 %%
+%% $Id$
 
 % symbol definitions
 
-\newcommand{\isasymzero}{\isatext{\textzerooldstyle}}  %requires textcomp
-\newcommand{\isasymone}{\isatext{\textoneoldstyle}}  %requires textcomp
-\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}}  %requires textcomp
-\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}}  %requires textcomp
-\newcommand{\isasymfour}{\isatext{\textfouroldstyle}}  %requires textcomp
-\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}}  %requires textcomp
-\newcommand{\isasymsix}{\isatext{\textsixoldstyle}}  %requires textcomp
-\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}}  %requires textcomp
-\newcommand{\isasymeight}{\isatext{\texteightoldstyle}}  %requires textcomp
-\newcommand{\isasymnine}{\isatext{\textnineoldstyle}}  %requires textcomp
+\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{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
 \newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
 \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
 \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
 \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
-\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires latexsym
+\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{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
 \newcommand{\isasymup}{\isamath{\uparrow}}
 \newcommand{\isasymUp}{\isamath{\Uparrow}}
 \newcommand{\isasymdown}{\isamath{\downarrow}}
 \newcommand{\isasymDown}{\isamath{\Downarrow}}
 \newcommand{\isasymupdown}{\isamath{\updownarrow}}

 \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{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel 
+\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel 
 \newcommand{\isasymColon}{\isamath{\mathrel{::}}}
 \newcommand{\isasymnot}{\isamath{\neg}}
 \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{\isasymbox}{\isamath{\Box}}  %requires latexsym
-\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}
 \newcommand{\isasymTurnstile}{\isamath{\models}}
 \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
 \newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
 \newcommand{\isasymstileturn}{\isamath{\dashv}}

 \newcommand{\isasymnotin}{\isamath{\notin}}
 \newcommand{\isasymsubset}{\isamath{\subset}}
 \newcommand{\isasymsupset}{\isamath{\supset}}
 \newcommand{\isasymsubseteq}{\isamath{\subseteq}}
 \newcommand{\isasymsupseteq}{\isamath{\supseteq}}
-\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
-\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires latexsym
+\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{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires amsmath
 \newcommand{\isasymuplus}{\isamath{\uplus}}
 \newcommand{\isasymUplus}{\isamath{\biguplus\,}}
 \newcommand{\isasymnoteq}{\isamath{\not=}}
 \newcommand{\isasymsim}{\isamath{\sim}}
 \newcommand{\isasymdoteq}{\isamath{\doteq}}

 \newcommand{\isasymcong}{\isamath{\cong}}
 \newcommand{\isasymsmile}{\isamath{\smile}}
 \newcommand{\isasymequiv}{\isamath{\equiv}}
 \newcommand{\isasymfrown}{\isamath{\frown}}
 \newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\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{\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}}
-\newcommand{\isasymrhd}{\isamath{\rhd}}
-\newcommand{\isasymunlhd}{\isamath{\unlhd}}
-\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\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{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
 \newcommand{\isasymsection}{\isatext{\rm\S}}
 \newcommand{\isasymparagraph}{\isatext{\rm\P}}
 \newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
 \newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
-\newcommand{\isasymeuro}{\isatext{\EUR}}  %requires marvosym
+\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}}  %requires greek babel
 \newcommand{\isasympounds}{\isamath{\pounds}}
 \newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
-\newcommand{\isasymcent}{\isatext{\cent}}  %requires wasysym
-\newcommand{\isasymcurrency}{\isatext{\currency}}  %requires wasysym
+\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
 \newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
 \newcommand{\isasymamalg}{\isamath{\amalg}}
-\newcommand{\isasymmho}{\isamath{\mho}}  %requires latexsym
-\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
-\newcommand{\isasymJoin}{\isamath{\Join}}  %requires latexsym
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
 \newcommand{\isasymwp}{\isamath{\wp}}
 \newcommand{\isasymwrong}{\isamath{\wr}}
 \newcommand{\isasymstruct}{\isamath{\diamond}}
 \newcommand{\isasymacute}{\isatext{\'\relax}}
 \newcommand{\isasymindex}{\isatext{\i}}
 \newcommand{\isasymdieresis}{\isatext{\"\relax}}
 \newcommand{\isasymcedilla}{\isatext{\c\relax}}
 \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
 \newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}