# HG changeset patch # User wenzelm # Date 1087582252 -7200 # Node ID 18ee74d6bba1acc40f67be7508c20dd53a750c3f # Parent 8159ade98144e447315cfe705a01a1235c8eeb20 improved comments -- required by 'isatool latex -o syms'; diff -r 8159ade98144 -r 18ee74d6bba1 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Fri Jun 18 20:07:59 2004 +0200 +++ b/lib/texinputs/isabellesym.sty Fri Jun 18 20:10:52 2004 +0200 @@ -7,16 +7,16 @@ % symbol definitions -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssym -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssym -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssym -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssym -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssym -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssym -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssym -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssym -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssym -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssym +\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}}} @@ -184,7 +184,7 @@ \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}} \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}} \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}} -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssym +\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb \newcommand{\isasymup}{\isamath{\uparrow}} \newcommand{\isasymUp}{\isamath{\Uparrow}} \newcommand{\isasymdown}{\isamath{\downarrow}} @@ -215,8 +215,8 @@ \newcommand{\isasymOr}{\isamath{\bigvee}} \newcommand{\isasymforall}{\isamath{\forall\,}} \newcommand{\isasymexists}{\isamath{\exists\,}} -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssym -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssym +\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}} @@ -237,8 +237,8 @@ \newcommand{\isasymsupset}{\isamath{\supset}} \newcommand{\isasymsubseteq}{\isamath{\subseteq}} \newcommand{\isasymsupseteq}{\isamath{\supseteq}} -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssym -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssym +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}} \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}} \newcommand{\isasyminter}{\isamath{\cap}} @@ -263,7 +263,7 @@ \newcommand{\isasymfrown}{\isamath{\frown}} \newcommand{\isasympropto}{\isamath{\propto}} \newcommand{\isasymsome}{\isamath{\epsilon\,}} -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssym +\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb \newcommand{\isasymbowtie}{\isamath{\bowtie}} \newcommand{\isasymprec}{\isamath{\prec}} \newcommand{\isasymsucc}{\isamath{\succ}} @@ -342,8 +342,8 @@ \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp \newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1 \newcommand{\isasymamalg}{\isamath{\amalg}} -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssym -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym +\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb +\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb \newcommand{\isasymwp}{\isamath{\wp}} \newcommand{\isasymwrong}{\isamath{\wr}} \newcommand{\isasymstruct}{\isamath{\diamond}}