%%

%% $Id$

%% Author: Markus Wenzel, TU Muenchen

%% License: GPL (GNU GENERAL PUBLIC LICENSE)

%%

%% definitions of standard Isabelle symbols

%%

\usepackage{latexsym}

%\usepackage{amssymb}

%\usepackage[latin1]{inputenc}

\newcommand{\bigsqcap}{\overline{|\,\,|}}  %an approximation ...

\newcommand{\isasymspacespace}{~~}

\newcommand{\isasymGamma}{$\Gamma$}

\newcommand{\isasymDelta}{$\Delta$}

\newcommand{\isasymTheta}{$\Theta$}

\newcommand{\isasymLambda}{$\Lambda$}

\newcommand{\isasymXi}{$\Xi$}

\newcommand{\isasymPi}{$\Pi$}

\newcommand{\isasymSigma}{$\Sigma$}

\newcommand{\isasymUpsilon}{$\Upsilon$}

\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{\isasymiota}{$\iota$}

\newcommand{\isasymkappa}{$\kappa$}

\newcommand{\isasymlambda}{$\lambda$}

\newcommand{\isasymmu}{$\mu$}

\newcommand{\isasymnu}{$\nu$}

\newcommand{\isasymxi}{$\xi$}

\newcommand{\isasympi}{$\pi$}

\newcommand{\isasymrho}{$\varrho$}

\newcommand{\isasymsigma}{$\sigma$}

\newcommand{\isasymtau}{$\tau$}

\newcommand{\isasymupsilon}{$\upsilon$}

\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{\isasymfrown}{\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}}

\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}

\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}

\newcommand{\isasymtop}{\emph{$\top$}}

\newcommand{\isasymcong}{\emph{$\cong$}}

\newcommand{\isasymclubsuit}{\emph{$\clubsuit$}}

\newcommand{\isasymdiamondsuit}{\emph{$\diamondsuit$}}

\newcommand{\isasymheartsuit}{\emph{$\heartsuit$}}

\newcommand{\isasymspadesuit}{\emph{$\spadesuit$}}

\newcommand{\isasymleftrightarrow}{\emph{$\leftrightarrow$}}

\newcommand{\isasymge}{\emph{$\ge$}}

\newcommand{\isasympropto}{\emph{$\propto$}}

\newcommand{\isasympartial}{\emph{$\partial$}}

\newcommand{\isasymdots}{\emph{$\dots$}}

\newcommand{\isasymaleph}{\emph{$\aleph$}}

\newcommand{\isasymIm}{\emph{$\Im$}}

\newcommand{\isasymRe}{\emph{$\Re$}}

\newcommand{\isasymwp}{\emph{$\wp$}}

\newcommand{\isasymemptyset}{\emph{$\emptyset$}}

\newcommand{\isasymangle}{\emph{$\angle$}}

\newcommand{\isasymnabla}{\emph{$\nabla$}}

\newcommand{\isasymProd}{\emph{$\prod\,$}}

\newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}}

\newcommand{\isasymUparrow}{\emph{$\Uparrow$}}

\newcommand{\isasymDownarrow}{\emph{$\Downarrow$}}

\newcommand{\isasymlozenge}{\emph{$\lozenge$}}

\newcommand{\isasymlangle}{\emph{$\langle$}}

\newcommand{\isasymrangle}{\emph{$\rangle$}}

\newcommand{\isasymSum}{\emph{$\sum\,$}}

\newcommand{\isasymintegral}{\emph{$\int\,$}}

\newcommand{\isasymdagger}{\emph{$\dagger$}}

\newcommand{\isasymsharp}{\emph{$\sharp$}}

\newcommand{\isasymstar}{\emph{$\star$}}

\newcommand{\isasymtriangleright}{\emph{$\triangleright$}}

\newcommand{\isasymlhd}{\emph{$\lhd$}}

\newcommand{\isasymtriangle}{\emph{$\triangle$}}

\newcommand{\isasymrhd}{\emph{$\rhd$}}

\newcommand{\isasymunlhd}{\emph{$\unlhd$}}

\newcommand{\isasymunrhd}{\emph{$\unrhd$}}

\newcommand{\isasymtriangleleft}{\emph{$\triangleleft$}}

\newcommand{\isasymnatural}{\emph{$\natural$}}

\newcommand{\isasymflat}{\emph{$\flat$}}

\newcommand{\isasymamalg}{\emph{$\amalg$}}

\newcommand{\isasymmho}{\emph{$\mho$}}

\newcommand{\isasymupdownarrow}{\emph{$\updownarrow$}}

\newcommand{\isasymlongmapsto}{\emph{$\longmapsto$}}

\newcommand{\isasymUpdownarrow}{\emph{$\Updownarrow$}}

\newcommand{\isasymhookleftarrow}{\emph{$\hookleftarrow$}}

\newcommand{\isasymhookrightarrow}{\emph{$\hookrightarrow$}}

\newcommand{\isasymrightleftharpoons}{\emph{$\rightleftharpoons$}}

\newcommand{\isasymleftharpoondown}{\emph{$\leftharpoondown$}}

\newcommand{\isasymrightharpoondown}{\emph{$\rightharpoondown$}}

\newcommand{\isasymleftharpoonup}{\emph{$\leftharpoonup$}}

\newcommand{\isasymrightharpoonup}{\emph{$\rightharpoonup$}}

\newcommand{\isasymasymp}{\emph{$\asymp$}}

\newcommand{\isasymminusplus}{\emph{$\mp$}}

\newcommand{\isasymbowtie}{\emph{$\bowtie$}}

\newcommand{\isasymcdots}{\emph{$\cdots$}}

\newcommand{\isasymodot}{\emph{$\odot$}}

\newcommand{\isasymsupset}{\emph{$\supset$}}

\newcommand{\isasymsupseteq}{\emph{$\supseteq$}}

\newcommand{\isasymsqsupset}{\emph{$\sqsupset$}}

\newcommand{\isasymsqsupseteq}{\emph{$\sqsupseteq$}}

\newcommand{\isasymll}{\emph{$\ll$}}

\newcommand{\isasymgg}{\emph{$\gg$}}

\newcommand{\isasymuplus}{\emph{$\uplus$}}

\newcommand{\isasymsmile}{\emph{$\smile$}}

\newcommand{\isasymsucceq}{\emph{$\succeq$}}

\newcommand{\isasymstileturn}{\emph{$\dashv$}}

\newcommand{\isasymOr}{\emph{$\bigvee$}}

\newcommand{\isasymbiguplus}{\emph{$\biguplus$}}

\newcommand{\isasymddagger}{\emph{$\ddagger$}}

\newcommand{\isasymJoin}{\emph{$\Join$}}

\newcommand{\isasymbool}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{B}$}}

\newcommand{\isasymcomplex}{\emph{$\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu$}}

\newcommand{\isasymnat}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{N}$}}

\newcommand{\isasymrat}{\emph{$\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu$}}

\newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}}

\newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}}

%require amssymb:

\newcommand{\isasymlesssim}{\emph{$\lesssim$}}

\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}}

\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}}

\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}}

\newcommand{\isasymtriangleq}{\emph{$\triangleq$}}