--- /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}}