%%
%% $Id$
%% Author: Markus Wenzel, TU Muenchen
%% License: GPL (GNU GENERAL PUBLIC LICENSE)
%%
%% definitions of standard Isabelle symbols
%%
% Required packages for unusual symbols -- see below for details.
%\usepackage{latexsym}
%\usepackage{amssymb}
%\usepackage[english]{babel}
%\usepackage[latin1]{inputenc}
%\usepackage[only,bigsqcap]{stmaryrd}
%\usepackage{wasysym}
% Note: \emph is important for proper spacing in fake math mode, it
% automatically inserts italic corrections around symbols wherever
% appropriate.
\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\,$}} %requires stmaryrd
\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{$\relbar$}}
\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
\newcommand{\isasymMidarrow}{\emph{$\Relbar$}}
\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
\newcommand{\isasymfrown}{\emph{$\frown$}}
\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
\newcommand{\isasymleadsto}{\emph{$\leadsto$}} %requires latexsym
\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$}} %requires latexsym
\newcommand{\isasymdiamond}{\emph{$\Diamond$}} %requires latexsym
\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$}}
\newcommand{\isasymbar}{\emph{$\mid$}}
\newcommand{\isasymhyphen}{\emph{\rm-}}
\newcommand{\isasymmacron}{\emph{\rm\=\relax}}
\newcommand{\isasymexclamdown}{\emph{\rm\textexclamdown}}
\newcommand{\isasymquestiondown}{\emph{\rm\textquestiondown}}
\newcommand{\isasymguillemotleft}{\emph{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\emph{\frqq}} %requires babel
\newcommand{\isasymdegree}{\emph{\rm\textdegree}} %requires latin1
\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}} %requires latin1
\newcommand{\isasymonequarter}{\emph{\rm\textonequarter}} %requires latin1
\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}} %requires latin1
\newcommand{\isasymonehalf}{\emph{\rm\textonehalf}} %requires latin1
\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}} %requires latin1
\newcommand{\isasymthreequarters}{\emph{\rm\textthreequarters}} %requires latin1
\newcommand{\isasymparagraph}{\emph{\P}}
\newcommand{\isasymregistered}{\emph{\rm\textregistered}}
\newcommand{\isasymordfeminine}{\emph{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\emph{\rm\textordmasculine}}
\newcommand{\isasymsection}{\emph{\S}}
\newcommand{\isasympounds}{\emph{$\pounds$}}
\newcommand{\isasymyen}{\emph{\yen}} %requires amssymb
\newcommand{\isasymcent}{\emph{\cent}} %requires wasysym
\newcommand{\isasymcurrency}{\emph{\currency}} %requires wasysym
\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$}} %requires amssym
\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$}} %requires latexsym
\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$}} %requires latexsym
\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$}} %requires latexsym
\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}$}}
\newcommand{\isasymlesssim}{\emph{$\lesssim$}} %requires amssymb
\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}} %requires amssymb
\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}} %requires amssymb
\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}} %requires amssymb
\newcommand{\isasymtriangleq}{\emph{$\triangleq$}} %requires amssymb
\newcommand{\isasymlparr}{\emph{$\mathopen{(\mkern-3mu\mid}$}}
\newcommand{\isasymrparr}{\emph{$\mathclose{\mid\mkern-3mu)}$}}