lib/texinputs/isabellesym.sty
author wenzelm
Sat, 30 Oct 1999 20:11:35 +0200
changeset 7979 bd9b0151c932
child 8147 b712b870a5d1
permissions -rw-r--r--
definitions of many Isabelle symbols;

%%
%% $Id$
%%
%% definitions of many Isabelle symbols
%%

\usepackage{latexsym}

\newcommand{\bigsqcap}{\overline{|\,\,|}}  %just a hack
%\def\textbrokenbar??? etc

\newcommand{\isasymspacespace}{~~}
\newcommand{\isasymGamma}{$\Gamma$}
\newcommand{\isasymDelta}{$\Delta$}
\newcommand{\isasymTheta}{$\Theta$}
\newcommand{\isasymLambda}{$\Lambda$}
\newcommand{\isasymPi}{$\Pi$}
\newcommand{\isasymSigma}{$\Sigma$}
\newcommand{\isasymPhi}{$\Phi$}
\newcommand{\isasymPsi}{$\Psi$}
\newcommand{\isasymOmega}{$\Omega$}
\newcommand{\isasymalpha}{$\alpha$}
\newcommand{\isasymbeta}{$\beta$}
\newcommand{\isasymgamma}{$\gamma$}
\newcommand{\isasymdelta}{$\delta$}
\newcommand{\isasymepsilon}{$\varepsilon$}
\newcommand{\isasymzeta}{$\zeta$}
\newcommand{\isasymeta}{$\eta$}
\newcommand{\isasymtheta}{$\vartheta$}
\newcommand{\isasymkappa}{$\kappa$}
\newcommand{\isasymlambda}{$\lambda$}
\newcommand{\isasymmu}{$\mu$}
\newcommand{\isasymnu}{$\nu$}
\newcommand{\isasymxi}{$\xi$}
\newcommand{\isasympi}{$\pi$}
\newcommand{\isasymrho}{$\rho$}
\newcommand{\isasymsigma}{$\sigma$}
\newcommand{\isasymtau}{$\tau$}
\newcommand{\isasymphi}{$\varphi$}
\newcommand{\isasymchi}{$\chi$}
\newcommand{\isasympsi}{$\psi$}
\newcommand{\isasymomega}{$\omega$}
\newcommand{\isasymnot}{\emph{$\neg$}}
\newcommand{\isasymand}{\emph{$\wedge$}}
\newcommand{\isasymor}{\emph{$\vee$}}
\newcommand{\isasymforall}{\emph{$\forall$}}
\newcommand{\isasymexists}{\emph{$\exists$}}
\newcommand{\isasymAnd}{\emph{$\bigwedge$}}
\newcommand{\isasymlceil}{\emph{$\lceil$}}
\newcommand{\isasymrceil}{\emph{$\rceil$}}
\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
\newcommand{\isasymturnstile}{\emph{$\vdash$}}
\newcommand{\isasymTurnstile}{\emph{$\models$}}
\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
\newcommand{\isasymcdot}{\emph{$\cdot$}}
\newcommand{\isasymin}{\emph{$\in$}}
\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
\newcommand{\isasyminter}{\emph{$\cap$}}
\newcommand{\isasymunion}{\emph{$\cup$}}
\newcommand{\isasymInter}{\emph{$\bigcap$}}
\newcommand{\isasymUnion}{\emph{$\bigcup$}}
\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
\newcommand{\isasymSqinter}{\emph{$\bigsqcap$}}
\newcommand{\isasymSqunion}{\emph{$\bigsqcup$}}
\newcommand{\isasymbottom}{\emph{$\bot$}}
\newcommand{\isasymdoteq}{\emph{$\doteq$}}
\newcommand{\isasymequiv}{\emph{$\equiv$}}
\newcommand{\isasymnoteq}{\emph{$\not=$}}
\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
\newcommand{\isasymprec}{\emph{$\prec$}}
\newcommand{\isasympreceq}{\emph{$\preceq$}}
\newcommand{\isasymsucc}{\emph{$\succ$}}
\newcommand{\isasymapprox}{\emph{$\approx$}}
\newcommand{\isasymsim}{\emph{$\sim$}}
\newcommand{\isasymsimeq}{\emph{$\simeq$}}
\newcommand{\isasymle}{\emph{$\le$}}
\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated
\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated
\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
\newcommand{\isasymbow}{\emph{$\frown$}}
\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
\newcommand{\isasymleadsto}{\emph{$\leadsto$}}
\newcommand{\isasymup}{\emph{$\uparrow$}}
\newcommand{\isasymdown}{\emph{$\downarrow$}}
\newcommand{\isasymnotin}{\emph{$\notin$}}
\newcommand{\isasymtimes}{\emph{$\times$}}
\newcommand{\isasymoplus}{\emph{$\oplus$}}
\newcommand{\isasymominus}{\emph{$\ominus$}}
\newcommand{\isasymotimes}{\emph{$\otimes$}}
\newcommand{\isasymoslash}{\emph{$\oslash$}}
\newcommand{\isasymsubset}{\emph{$\subset$}}
\newcommand{\isasyminfinity}{\emph{$\infty$}}
\newcommand{\isasymbox}{\emph{$\Box$}}
\newcommand{\isasymdiamond}{\emph{$\Diamond$}}
\newcommand{\isasymcirc}{\emph{$\circ$}}
\newcommand{\isasymbullet}{\emph{$\bullet$}}
\newcommand{\isasymparallel}{\emph{$\parallel$}}
\newcommand{\isasymsurd}{\emph{$\surd$}}
\newcommand{\isasymcopyright}{\emph{\copyright}}

\newcommand{\isasymplusminus}{\emph{$\pm$}}
\newcommand{\isasymdiv}{\emph{$\div$}}
\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
%requires OT1 encoding:
\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}}
\newcommand{\isasymhyphen}{-}
\newcommand{\isasymmacron}{\={}}
\newcommand{\isasymexclamdown}{\emph{\textexclamdown}}
\newcommand{\isasymquestiondown}{\emph{\textquestiondown}}
%requires OT1 encoding:
\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}}
%requires OT1 encoding:
\newcommand{\isasymguillemotright}{\emph{\guillemotright}}
%should be available (?):
\newcommand{\isasymdegree}{\emph{\textdegree}}
\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}
\newcommand{\isasymonequarter}{\emph{\textonequarter}}
\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}
\newcommand{\isasymonehalf}{\emph{\textonehalf}}
\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}
\newcommand{\isasymthreequarters}{\emph{\textthreequarters}}
\newcommand{\isasymparagraph}{\emph{\P}}
\newcommand{\isasymregistered}{\emph{\textregistered}}
%should be available (?):
\newcommand{\isasymordfeminine}{\emph{\textordfeminine}}
%should be available (?):
\newcommand{\isasymordmasculine}{\emph{\textordmasculine}}
\newcommand{\isasymsection}{\S}
\newcommand{\isasympounds}{\emph{$\pounds$}}
%requires OT1 encoding:
\newcommand{\isasymyen}{\emph{\textyen}}
%requires OT1 encoding:
\newcommand{\isasymcent}{\emph{\textcent}}
%requires OT1 encoding:
\newcommand{\isasymcurrency}{\emph{\textcurrency}}