diff -r 1b99ee57d131 -r bd9b0151c932 lib/texinputs/isabellesym.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/texinputs/isabellesym.sty Sat Oct 30 20:11:35 1999 +0200 @@ -0,0 +1,148 @@ +%% +%% $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}}