\documentclass[11pt,a4paper,fleqn]{article}
\usepackage{english,a4,bbb,../pdfsetup}
\usepackage[latin1]{inputenc}
\makeatletter
%%% layout
\sloppy
\parindent 0pt
\parskip 0.5ex
%%% text mode
\newcommand{\B}[1]{\textbf{#1}}
\newcommand{\TT}[1]{\ifmmode\mbox{\texttt{#1}}\else\texttt{#1}\fi}
\newcommand{\E}[1]{\emph{#1}}
\renewcommand{\P}[1]{\textsc{#1}}
\renewcommand{\labelenumi}{(\theenumi)}
\newcommand{\dfn}[1]{{\bf #1}}
\newcommand{\thy}[1]{\mbox{\sc #1}}
%\newcommand{\thy}[1]{\mbox{\textsc{#1}}}
\newcommand{\IHOL}{\thy{ihol}}
\newcommand{\SIHOL}{\thy{sihol}}
\newcommand{\HOL}{\thy{hol}}
\newcommand{\HOLBB}{\thy{hol88}}
\newcommand{\FOL}{\thy{fol}}
\newcommand{\SET}{\thy{set}}
\newcommand{\Pure}{\thy{Pure}}
\newcommand{\secref}[1]{\S\ref{#1}}
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
%from alltt.sty
\def\docspecials{\do\ \do\$\do\&%
\do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~}
\newenvironment{asc}{\small\trivlist \item[]\if@minipage\else\vskip\parskip\fi
\leftskip\@totalleftmargin\rightskip\z@
\parindent\z@\parfillskip\@flushglue\parskip\z@
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
\obeylines \tt \catcode``=13 \@noligs \let\do\@makeother \docspecials
\frenchspacing\@vobeyspaces}{\endtrivlist}
\newenvironment{ascbox}{\vbox\bgroup\begin{asc}}{\end{asc}\egroup}
\newcommand{\brk}{\end{ascbox}\vskip-20pt\begin{ascbox}}
\newcommand{\out}[1]{{\fontfamily{cmtt}\fontseries{m}\fontshape{sl}\selectfont\ \ #1}}
% warning environment
\newcommand{\dbend}{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
\newenvironment{warning}{\medskip\medbreak\begingroup \clubpenalty=10000
\noindent \hangindent1.5em \hangafter=-2
\hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
{\par\endgroup\medbreak}
\newcommand{\Isa}{{\sc Isabelle}}
\newcommand{\ML}{{\sc ml}}
\newcommand{\Haskell}{{\rm Haskell}}
\newcommand{\IMP}{"`$\Longrightarrow$"'}
\newcommand{\PMI}{"`$\Longleftarrow$"'}
%%% math mode
%% generic defs
\newcommand{\nquad}{\hskip-1em}
\newcommand{\fct}[1]{\mathop{\rm #1}\nolimits}
\newcommand{\idt}[1]{{\mathord{\it #1}}}
\newcommand{\syn}[1]{{\mathord{\it #1}}}
\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\rmtext}[1]{\mbox{\rm #1}}
%\newcommand{\mtt}[1]{\mbox{\tt #1}}
\newcommand{\falls}{\text{falls }}
\newcommand{\sonst}{\text{sonst}}
\newcommand{\Bool}{\bbbB}
\newcommand{\Nat}{\bbbN}
\newcommand{\Natz}{{\bbbN_0}}
\newcommand{\Rat}{\bbbQ}
\newcommand{\Real}{\bbbR}
\newcommand{\dt}{{\mathpunct.}}
\newcommand{\Gam}{\Gamma}
\renewcommand{\epsilon}{\varepsilon}
\renewcommand{\phi}{\varphi}
\renewcommand{\rho}{\varrho}
\newcommand{\eset}{{\{\}}}
\newcommand{\etuple}{{\langle\rangle}}
\newcommand{\dfneq}{\mathbin{\mathord:\mathord=}}
\newcommand{\impl}{\Longrightarrow}
\renewcommand{\iff}{{\;\;\mathord{\Longleftrightarrow}\;\;}}
\newcommand{\dfniff}{{\;\;\mathord:\mathord{\Longleftrightarrow}\;\;}}
\renewcommand{\land}{\mathrel{\,\wedge\,}}
\renewcommand{\lor}{\mathrel{\,\vee\,}}
\newcommand{\iso}{\cong}
\newcommand{\union}{\cup}
\newcommand{\sunion}{\mathbin{\;\cup\;}}
\newcommand{\dunion}{\mathbin{\dot\union}}
\newcommand{\Union}{\bigcup}
\newcommand{\inter}{\cap}
\newcommand{\where}{\mathrel|}
\newcommand{\pto}{\rightharpoonup}
\newcommand{\comp}{\circ}
\newcommand{\aaast}{{\mathord*\mathord*\mathord*}}
\newcommand{\all}[1]{\forall #1\dt\;}
\newcommand{\ex}[1]{\exists #1\dt\;}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
\newcommand\lbrakk{\mathopen{[\![}}
\newcommand\rbrakk{\mathclose{]\!]}}
\newcommand{\unif}{\mathrel{=^?}}
\newcommand{\notunif}{\mathrel{{\not=}^?}}
\newcommand{\incompat}{\mathrel{\#}}
%% specific defs
\newcommand{\PLUS}{\mathord{\langle{+}\rangle}}
\newcommand{\TIMES}{\mathord{\langle{*}\rangle}}
% IHOL
\newcommand{\TV}{\fct{TV}}
\newcommand{\FV}{\fct{FV}}
\newcommand{\BV}{\fct{BV}}
\newcommand{\VN}{\fct{VN}}
\newcommand{\AT}{\fct{AT}}
\newcommand{\STV}{\fct{STV}}
\newcommand{\TyVars}{\syn{TyVars}}
\newcommand{\TyNames}{\syn{TyNames}}
\newcommand{\TyCons}{\syn{TyCons}}
\newcommand{\TyConsSg}{\TyCons_\Sigma}
\newcommand{\Types}{\syn{Types}}
\newcommand{\TypesSg}{\Types_\Sigma}
\newcommand{\GrTypes}{\syn{GrTypes}}
\newcommand{\GrTypesSg}{\GrTypes_\Sigma}
\newcommand{\VarNames}{\syn{VarNames}}
\newcommand{\Vars}{\syn{Vars}}
\newcommand{\VarsSg}{\Vars_\Sigma}
\newcommand{\GrVars}{\syn{GrVars}}
\newcommand{\GrVarsSg}{\GrVars_\Sigma}
\newcommand{\ConstNames}{\syn{ConstNames}}
\newcommand{\Consts}{\syn{Consts}}
\newcommand{\ConstsSg}{\Consts_\Sigma}
\newcommand{\GrConsts}{\syn{GrConsts}}
\newcommand{\GrConstsSg}{\GrConsts_\Sigma}
\newcommand{\Terms}{\syn{Terms}}
\newcommand{\TermsSg}{\Terms_\Sigma}
\newcommand{\GrTerms}{\syn{GrTerms}}
\newcommand{\GrTermsSg}{\GrTerms_\Sigma}
\newcommand{\Forms}{\syn{Forms}}
\newcommand{\FormsTh}{\Forms_\Theta}
\newcommand{\Seqs}{\syn{Seqs}}
\newcommand{\SeqsTh}{\Seqs_\Theta}
\newcommand{\Axms}{\syn{Axms}}
\newcommand{\AxmsTh}{\Axms_\Theta}
\newcommand{\Thms}{\syn{Thms}}
\newcommand{\ThmsTh}{\Thms_\Theta}
\newcommand{\U}{{\cal U}}
\newcommand{\UU}{\bbbU}
\newcommand{\ty}{{\mathbin{\,:\,}}}
\newcommand{\typ}[1]{{\mathord{\sl #1}}}
\newcommand{\tap}{\mathord{\,}}
\newcommand{\prop}{\typ{prop}}
\newcommand{\itself}{\typ{itself}}
\newcommand{\cnst}[1]{{\mathord{\sl #1}}}
\newcommand{\ap}{\mathbin{}}
\newcommand{\To}{\Rightarrow}
\newcommand{\Eq}{\equiv}
\newcommand{\Impl}{\Rightarrow}
\newcommand{\Forall}{\mathop{\textstyle\bigwedge}}
\newcommand{\All}[1]{\Forall #1\dt}
\newcommand{\True}{\top}
\newcommand{\False}{\bot}
\newcommand{\Univ}{{\top\!\!\!\!\top}}
\newcommand{\Conj}{\wedge}
\newcommand{\TYPE}{\cnst{TYPE}}
% rules
\newcommand{\Axm}{\rmtext{Axm}}
\newcommand{\Assm}{\rmtext{Assm}}
\newcommand{\Mon}{\rmtext{Mon}}
\newcommand{\ImplI}{\mathord{\Impl}\rmtext{I}}
\newcommand{\ImplE}{\mathord{\Impl}\rmtext{E}}
\newcommand{\ImplMP}{\rmtext{MP}}
\newcommand{\ImplRefl}{\mathord{\Impl}\rmtext{Refl}}
\newcommand{\ImplTrans}{\mathord{\Impl}\rmtext{Trans}}
\newcommand{\EqRefl}{\mathord{\Eq}\rmtext{Refl}}
\newcommand{\EqTrans}{\mathord{\Eq}\rmtext{Trans}}
\newcommand{\EqSym}{\mathord{\Eq}\rmtext{Sym}}
\newcommand{\EqApp}{\mathord{\Eq}\rmtext{App}}
\newcommand{\EqAbs}{\mathord{\Eq}\rmtext{Abs}}
\newcommand{\Eqa}{\mathord{\Eq}\alpha}
\newcommand{\Eqb}{\mathord{\Eq}\beta}
\newcommand{\Eqe}{\mathord{\Eq}\eta}
\newcommand{\Ext}{\rmtext{Ext}}
\newcommand{\EqI}{\mathord{\Eq}\rmtext{I}}
\newcommand{\EqMP}{\mathord{\Eq}\rmtext{MP}}
\newcommand{\EqUnfold}{\mathord{\Eq}\rmtext{Unfold}}
\newcommand{\EqFold}{\mathord{\Eq}\rmtext{Fold}}
\newcommand{\AllI}{\mathord{\Forall}\rmtext{I}}
\newcommand{\AllE}{\mathord{\Forall}\rmtext{E}}
\newcommand{\TypInst}{\rmtext{TypInst}}
\newcommand{\Inst}{\rmtext{Inst}}
\newcommand{\TrueI}{\True\rmtext{I}}
\newcommand{\FalseE}{\False\rmtext{E}}
\newcommand{\UnivI}{\Univ\rmtext{I}}
\newcommand{\ConjI}{\mathord{\Conj}\rmtext{I}}
\newcommand{\ConjE}{\mathord{\Conj}\rmtext{E}}
\newcommand{\ConjProj}{\mathord{\Conj}\rmtext{Proj}}
\newcommand{\ImplCurry}{\mathord{\Impl}\rmtext{Curry}}
\newcommand{\ImplUncurry}{\mathord{\Impl}\rmtext{Uncurry}}
\newcommand{\CImplI}{\mathord{\Conj}\mathord{\Impl}\rmtext{I}}
\newcommand{\CImplE}{\mathord{\Conj}\mathord{\Impl}\rmtext{E}}
\newcommand{\Subclass}{\rmtext{Subclass}}
\newcommand{\Subsort}{\rmtext{Subsort}}
\newcommand{\VarSort}{\rmtext{VarSort}}
\newcommand{\Arity}{\rmtext{Arity}}
\newcommand{\SortMP}{\rmtext{SortMP}}
\newcommand{\TopSort}{\rmtext{TopSort}}
\newcommand{\OfSort}{\rmtext{OfSort}}
\newcommand{\infr}{{\mathrel/}}
\newcommand{\einfr}{{}{\mathrel/}}
\newcommand{\drv}{\mathrel{\vdash}}
\newcommand{\Drv}[1]{\mathrel{\mathord{\drv}_{#1}}}
\newcommand{\Gdrv}{\Gam\drv}
\newcommand{\edrv}{\mathop{\drv}\nolimits}
\newcommand{\Edrv}[1]{\mathop{\drv}\nolimits_{#1}}
\newcommand{\notEdrv}[1]{\mathop{\not\drv}\nolimits_{#1}}
\newcommand{\lsem}{\lbrakk}
\newcommand{\rsem}{\rbrakk}
\newcommand{\sem}[1]{{\lsem #1\rsem}}
\newcommand{\vld}{\mathrel{\models}}
\newcommand{\Vld}[1]{\mathrel{\mathord{\models}_#1}}
\newcommand{\Evld}[1]{\mathop{\vld}\nolimits_{#1}}
\newcommand{\notEvld}[1]{\mathop{\not\vld}\nolimits_{#1}}
\newcommand{\EQ}{\fct{EQ}}
\newcommand{\IMPL}{\fct{IMPL}}
\newcommand{\ALL}{\fct{ALL}}
\newcommand{\extcv}{\mathrel{\unlhd}}
\newcommand{\weakth}{\preceq}
\newcommand{\eqvth}{\approx}
\newcommand{\extdcli}{\mathrel{<_{\rm dcl}^1}}
\newcommand{\extdcl}{\mathrel{\le_{\rm dcl}}}
\newcommand{\extdfni}{\mathrel{<_{\rm dfn}^1}}
\newcommand{\extdfn}{\mathrel{\le_{\rm dfn}}}
\newcommand{\extsdfn}{\mathrel{\le_{\rm sdfn}}}
\newcommand{\extqdfn}{\mathrel{\le_{\rm qdfn}}}
\newcommand{\lvarbl}{\langle}
\newcommand{\rvarbl}{\rangle}
\newcommand{\varbl}[1]{{\lvarbl #1\rvarbl}}
\newcommand{\up}{{\scriptstyle\mathord\uparrow}}
\newcommand{\down}{{\scriptstyle\mathord\downarrow}}
\newcommand{\Down}{{\mathord\downarrow}}
\newcommand{\Sle}{{\mathrel{\le_S}}}
\newcommand{\Classes}{\syn{Classes}}
\newcommand{\ClassNames}{\syn{ClassNames}}
\newcommand{\Sorts}{\syn{Sorts}}
\newcommand{\TyVarNames}{\syn{TyVarNames}}
\newcommand{\STyVars}{\syn{STyVars}}
\newcommand{\STyArities}{\syn{STyArities}}
\newcommand{\STypes}{\syn{STypes}}
\newcommand{\SVars}{\syn{SVars}}
\newcommand{\SConsts}{\syn{SConsts}}
\newcommand{\STerms}{\syn{STerms}}
\newcommand{\SForms}{\syn{SForms}}
\newcommand{\SAxms}{\syn{SAxms}}
\newcommand{\T}{{\cal T}}
\newcommand{\cls}[1]{{\mathord{\sl #1}}}
\newcommand{\intsrt}{\sqcap}
\newcommand{\Intsrt}{{\mathop\sqcap}}
\newcommand{\subcls}{\preceq}
\newcommand{\Subcls}[1]{\mathrel{\subcls_{#1}}}
\newcommand{\subsrt}{\sqsubseteq}
\newcommand{\Subsrt}[1]{\mathrel{\subsrt_{#1}}}
\newcommand{\subsrtp}{\sqsubset}
\newcommand{\eqvsrt}{\approx}
\newcommand{\topsrt}{\top}
\newcommand{\srt}{\ty}
\newcommand{\sct}[1]{{\bf #1}}
\newcommand{\CLASSES}{\sct{classes}}
\newcommand{\CLASSREL}{\sct{classrel}}
\newcommand{\TYPES}{\sct{types}}
\newcommand{\ARITIES}{\sct{arities}}
\newcommand{\CONSTS}{\sct{consts}}
\newcommand{\AXIOMS}{\sct{axioms}}
\newcommand{\DEFNS}{\sct{defns}}
\newcommand{\AXCLASS}{\sct{axclass}}
\newcommand{\INSTANCE}{\sct{instance}}
\newcommand{\Srt}{{\mathbin{\,:\,}}}
\newcommand{\insrt}[2]{{\mathopen{(\!|} #1 \Srt #2 \mathclose{|\!)}}}
\newcommand{\ofsrt}[2]{{\mathopen{\langle\!|} #1 \Srt #2 \mathclose{|\!\rangle}}}
\newcommand{\injV}{{\iota_V}}
\newcommand{\inj}{\iota}
\newcommand{\injC}{{\iota_C}}
\newcommand{\I}{{\cal I}}
\newcommand{\C}{{\cal C}}
\newcommand{\Sdrv}{\mathrel{\vdash\!\!\!\vdash}}
\newcommand{\SDrv}[1]{\mathrel{\mathord{\Sdrv}_{#1}}}
\newcommand{\SGdrv}{\Gam\Sdrv}
\newcommand{\Sedrv}{\mathop{\Sdrv}\nolimits}
\newcommand{\SEdrv}[1]{\mathop{\Sdrv}\nolimits_{#1}}
\newcommand{\SSubclass}{\rmtext{S-Subclass}}
\newcommand{\SSubsort}{\rmtext{S-Subsort}}
\newcommand{\SVarSort}{\rmtext{S-VarSort}}
\newcommand{\SArity}{\rmtext{S-Arity}}
\newcommand{\SSortMP}{\rmtext{S-SortMP}}
\newcommand{\STopSort}{\rmtext{S-TopSort}}
\newcommand{\SOfSort}{\rmtext{S-OfSort}}
\makeatother
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: