doc-src/AxClass/style.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/style.tex	Mon May 12 17:53:36 1997 +0200
@@ -0,0 +1,362 @@
+
+\documentclass[11pt,a4paper,fleqn]{article}
+\usepackage[latin1]{inputenc}
+\usepackage{english}
+\usepackage{a4}
+\usepackage{alltt}
+\usepackage{bbb}
+
+
+\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
+