doc-src/AxClass/style.tex
author wenzelm
Tue, 20 May 1997 19:29:50 +0200
changeset 3257 4e3724e0659f
parent 3167 4e1eae442821
child 3286 321f49dae373
permissions -rw-r--r--
README generation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3167
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     2
\documentclass[11pt,a4paper,fleqn]{article}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     3
\usepackage[latin1]{inputenc}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     4
\usepackage{english}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     5
\usepackage{a4}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     6
\usepackage{alltt}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     7
\usepackage{bbb}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     8
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     9
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    10
\makeatletter
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    11
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    12
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    13
%%% layout
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    14
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    15
\sloppy
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    16
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    17
\parindent 0pt
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    18
\parskip 0.5ex
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    19
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    20
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    21
%%% text mode
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    22
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    23
\newcommand{\B}[1]{\textbf{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    24
\newcommand{\TT}[1]{\ifmmode\mbox{\texttt{#1}}\else\texttt{#1}\fi}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    25
\newcommand{\E}[1]{\emph{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    26
\renewcommand{\P}[1]{\textsc{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    27
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    28
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    29
\renewcommand{\labelenumi}{(\theenumi)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    30
\newcommand{\dfn}[1]{{\bf #1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    31
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    32
\newcommand{\thy}[1]{\mbox{\sc #1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    33
%\newcommand{\thy}[1]{\mbox{\textsc{#1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    34
\newcommand{\IHOL}{\thy{ihol}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    35
\newcommand{\SIHOL}{\thy{sihol}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    36
\newcommand{\HOL}{\thy{hol}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    37
\newcommand{\HOLBB}{\thy{hol88}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    38
\newcommand{\FOL}{\thy{fol}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    39
\newcommand{\SET}{\thy{set}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    40
\newcommand{\Pure}{\thy{Pure}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    41
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    42
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    43
\newcommand{\secref}[1]{\S\ref{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    44
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    45
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    46
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    47
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    48
%from alltt.sty
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    49
\def\docspecials{\do\ \do\$\do\&%
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    50
  \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    51
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    52
\newenvironment{asc}{\small\trivlist \item[]\if@minipage\else\vskip\parskip\fi
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    53
\leftskip\@totalleftmargin\rightskip\z@
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    54
\parindent\z@\parfillskip\@flushglue\parskip\z@
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    55
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    56
\obeylines \tt \catcode``=13 \@noligs \let\do\@makeother \docspecials
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    57
\frenchspacing\@vobeyspaces}{\endtrivlist}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    58
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    59
\newenvironment{ascbox}{\vbox\bgroup\begin{asc}}{\end{asc}\egroup}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    60
\newcommand{\brk}{\end{ascbox}\vskip-20pt\begin{ascbox}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    61
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    62
\newcommand{\out}[1]{{\fontfamily{cmtt}\fontseries{m}\fontshape{sl}\selectfont\ \ #1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    63
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    64
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    65
% warning environment
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    66
\newcommand{\dbend}{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    67
\newenvironment{warning}{\medskip\medbreak\begingroup \clubpenalty=10000
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    68
    \noindent \hangindent1.5em \hangafter=-2
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    69
    \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    70
  {\par\endgroup\medbreak}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    71
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    72
\newcommand{\Isa}{{\sc Isabelle}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    73
\newcommand{\ML}{{\sc ml}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    74
\newcommand{\Haskell}{{\rm Haskell}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    75
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    76
\newcommand{\IMP}{"`$\Longrightarrow$"'}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    77
\newcommand{\PMI}{"`$\Longleftarrow$"'}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    78
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    79
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    80
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    81
%%% math mode
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    82
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    83
%% generic defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    84
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    85
\newcommand{\nquad}{\hskip-1em}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    86
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    87
\newcommand{\fct}[1]{\mathop{\rm #1}\nolimits}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    88
\newcommand{\idt}[1]{{\mathord{\it #1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    89
\newcommand{\syn}[1]{{\mathord{\it #1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    90
\newcommand{\text}[1]{\mbox{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    91
\newcommand{\rmtext}[1]{\mbox{\rm #1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    92
%\newcommand{\mtt}[1]{\mbox{\tt #1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    93
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    94
\newcommand{\falls}{\text{falls }}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    95
\newcommand{\sonst}{\text{sonst}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    96
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    97
\newcommand{\Bool}{\bbbB}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    98
\newcommand{\Nat}{\bbbN}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    99
\newcommand{\Natz}{{\bbbN_0}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   100
\newcommand{\Rat}{\bbbQ}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   101
\newcommand{\Real}{\bbbR}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   102
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   103
\newcommand{\dt}{{\mathpunct.}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   104
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   105
\newcommand{\Gam}{\Gamma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   106
\renewcommand{\epsilon}{\varepsilon}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   107
\renewcommand{\phi}{\varphi}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   108
\renewcommand{\rho}{\varrho}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   109
\newcommand{\eset}{{\{\}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   110
\newcommand{\etuple}{{\langle\rangle}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   111
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   112
\newcommand{\dfneq}{\mathbin{\mathord:\mathord=}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   113
\newcommand{\impl}{\Longrightarrow}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   114
\renewcommand{\iff}{{\;\;\mathord{\Longleftrightarrow}\;\;}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   115
\newcommand{\dfniff}{{\;\;\mathord:\mathord{\Longleftrightarrow}\;\;}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   116
\renewcommand{\land}{\mathrel{\,\wedge\,}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   117
\renewcommand{\lor}{\mathrel{\,\vee\,}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   118
\newcommand{\iso}{\cong}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   119
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   120
\newcommand{\union}{\cup}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   121
\newcommand{\sunion}{\mathbin{\;\cup\;}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   122
\newcommand{\dunion}{\mathbin{\dot\union}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   123
\newcommand{\Union}{\bigcup}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   124
\newcommand{\inter}{\cap}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   125
\newcommand{\where}{\mathrel|}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   126
\newcommand{\pto}{\rightharpoonup}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   127
\newcommand{\comp}{\circ}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   128
\newcommand{\aaast}{{\mathord*\mathord*\mathord*}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   129
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   130
\newcommand{\all}[1]{\forall #1\dt\;}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   131
\newcommand{\ex}[1]{\exists #1\dt\;}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   132
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   133
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   134
\newcommand\lbrakk{\mathopen{[\![}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   135
\newcommand\rbrakk{\mathclose{]\!]}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   136
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   137
\newcommand{\unif}{\mathrel{=^?}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   138
\newcommand{\notunif}{\mathrel{{\not=}^?}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   139
\newcommand{\incompat}{\mathrel{\#}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   140
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   141
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   142
%% specific defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   143
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   144
\newcommand{\PLUS}{\mathord{\langle{+}\rangle}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   145
\newcommand{\TIMES}{\mathord{\langle{*}\rangle}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   146
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   147
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   148
% IHOL
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   149
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   150
\newcommand{\TV}{\fct{TV}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   151
\newcommand{\FV}{\fct{FV}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   152
\newcommand{\BV}{\fct{BV}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   153
\newcommand{\VN}{\fct{VN}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   154
\newcommand{\AT}{\fct{AT}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   155
\newcommand{\STV}{\fct{STV}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   156
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   157
\newcommand{\TyVars}{\syn{TyVars}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   158
\newcommand{\TyNames}{\syn{TyNames}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   159
\newcommand{\TyCons}{\syn{TyCons}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   160
\newcommand{\TyConsSg}{\TyCons_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   161
\newcommand{\Types}{\syn{Types}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   162
\newcommand{\TypesSg}{\Types_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   163
\newcommand{\GrTypes}{\syn{GrTypes}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   164
\newcommand{\GrTypesSg}{\GrTypes_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   165
\newcommand{\VarNames}{\syn{VarNames}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   166
\newcommand{\Vars}{\syn{Vars}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   167
\newcommand{\VarsSg}{\Vars_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   168
\newcommand{\GrVars}{\syn{GrVars}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   169
\newcommand{\GrVarsSg}{\GrVars_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   170
\newcommand{\ConstNames}{\syn{ConstNames}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   171
\newcommand{\Consts}{\syn{Consts}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   172
\newcommand{\ConstsSg}{\Consts_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   173
\newcommand{\GrConsts}{\syn{GrConsts}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   174
\newcommand{\GrConstsSg}{\GrConsts_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   175
\newcommand{\Terms}{\syn{Terms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   176
\newcommand{\TermsSg}{\Terms_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   177
\newcommand{\GrTerms}{\syn{GrTerms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   178
\newcommand{\GrTermsSg}{\GrTerms_\Sigma}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   179
\newcommand{\Forms}{\syn{Forms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   180
\newcommand{\FormsTh}{\Forms_\Theta}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   181
\newcommand{\Seqs}{\syn{Seqs}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   182
\newcommand{\SeqsTh}{\Seqs_\Theta}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   183
\newcommand{\Axms}{\syn{Axms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   184
\newcommand{\AxmsTh}{\Axms_\Theta}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   185
\newcommand{\Thms}{\syn{Thms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   186
\newcommand{\ThmsTh}{\Thms_\Theta}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   187
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   188
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   189
\newcommand{\U}{{\cal U}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   190
\newcommand{\UU}{\bbbU}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   191
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   192
\newcommand{\ty}{{\mathbin{\,:\,}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   193
\newcommand{\typ}[1]{{\mathord{\sl #1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   194
\newcommand{\tap}{\mathord{\,}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   195
\newcommand{\prop}{\typ{prop}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   196
\newcommand{\itself}{\typ{itself}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   197
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   198
\newcommand{\cnst}[1]{{\mathord{\sl #1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   199
\newcommand{\ap}{\mathbin{}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   200
\newcommand{\To}{\Rightarrow}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   201
\newcommand{\Eq}{\equiv}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   202
\newcommand{\Impl}{\Rightarrow}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   203
\newcommand{\Forall}{\mathop{\textstyle\bigwedge}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   204
\newcommand{\All}[1]{\Forall #1\dt}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   205
\newcommand{\True}{\top}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   206
\newcommand{\False}{\bot}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   207
\newcommand{\Univ}{{\top\!\!\!\!\top}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   208
\newcommand{\Conj}{\wedge}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   209
\newcommand{\TYPE}{\cnst{TYPE}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   210
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   211
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   212
% rules
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   213
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   214
\newcommand{\Axm}{\rmtext{Axm}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   215
\newcommand{\Assm}{\rmtext{Assm}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   216
\newcommand{\Mon}{\rmtext{Mon}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   217
\newcommand{\ImplI}{\mathord{\Impl}\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   218
\newcommand{\ImplE}{\mathord{\Impl}\rmtext{E}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   219
\newcommand{\ImplMP}{\rmtext{MP}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   220
\newcommand{\ImplRefl}{\mathord{\Impl}\rmtext{Refl}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   221
\newcommand{\ImplTrans}{\mathord{\Impl}\rmtext{Trans}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   222
\newcommand{\EqRefl}{\mathord{\Eq}\rmtext{Refl}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   223
\newcommand{\EqTrans}{\mathord{\Eq}\rmtext{Trans}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   224
\newcommand{\EqSym}{\mathord{\Eq}\rmtext{Sym}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   225
\newcommand{\EqApp}{\mathord{\Eq}\rmtext{App}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   226
\newcommand{\EqAbs}{\mathord{\Eq}\rmtext{Abs}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   227
\newcommand{\Eqa}{\mathord{\Eq}\alpha}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   228
\newcommand{\Eqb}{\mathord{\Eq}\beta}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   229
\newcommand{\Eqe}{\mathord{\Eq}\eta}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   230
\newcommand{\Ext}{\rmtext{Ext}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   231
\newcommand{\EqI}{\mathord{\Eq}\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   232
\newcommand{\EqMP}{\mathord{\Eq}\rmtext{MP}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   233
\newcommand{\EqUnfold}{\mathord{\Eq}\rmtext{Unfold}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   234
\newcommand{\EqFold}{\mathord{\Eq}\rmtext{Fold}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   235
\newcommand{\AllI}{\mathord{\Forall}\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   236
\newcommand{\AllE}{\mathord{\Forall}\rmtext{E}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   237
\newcommand{\TypInst}{\rmtext{TypInst}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   238
\newcommand{\Inst}{\rmtext{Inst}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   239
\newcommand{\TrueI}{\True\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   240
\newcommand{\FalseE}{\False\rmtext{E}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   241
\newcommand{\UnivI}{\Univ\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   242
\newcommand{\ConjI}{\mathord{\Conj}\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   243
\newcommand{\ConjE}{\mathord{\Conj}\rmtext{E}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   244
\newcommand{\ConjProj}{\mathord{\Conj}\rmtext{Proj}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   245
\newcommand{\ImplCurry}{\mathord{\Impl}\rmtext{Curry}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   246
\newcommand{\ImplUncurry}{\mathord{\Impl}\rmtext{Uncurry}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   247
\newcommand{\CImplI}{\mathord{\Conj}\mathord{\Impl}\rmtext{I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   248
\newcommand{\CImplE}{\mathord{\Conj}\mathord{\Impl}\rmtext{E}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   249
\newcommand{\Subclass}{\rmtext{Subclass}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   250
\newcommand{\Subsort}{\rmtext{Subsort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   251
\newcommand{\VarSort}{\rmtext{VarSort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   252
\newcommand{\Arity}{\rmtext{Arity}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   253
\newcommand{\SortMP}{\rmtext{SortMP}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   254
\newcommand{\TopSort}{\rmtext{TopSort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   255
\newcommand{\OfSort}{\rmtext{OfSort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   256
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   257
\newcommand{\infr}{{\mathrel/}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   258
\newcommand{\einfr}{{}{\mathrel/}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   259
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   260
\newcommand{\drv}{\mathrel{\vdash}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   261
\newcommand{\Drv}[1]{\mathrel{\mathord{\drv}_{#1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   262
\newcommand{\Gdrv}{\Gam\drv}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   263
\newcommand{\edrv}{\mathop{\drv}\nolimits}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   264
\newcommand{\Edrv}[1]{\mathop{\drv}\nolimits_{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   265
\newcommand{\notEdrv}[1]{\mathop{\not\drv}\nolimits_{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   266
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   267
\newcommand{\lsem}{\lbrakk}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   268
\newcommand{\rsem}{\rbrakk}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   269
\newcommand{\sem}[1]{{\lsem #1\rsem}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   270
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   271
\newcommand{\vld}{\mathrel{\models}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   272
\newcommand{\Vld}[1]{\mathrel{\mathord{\models}_#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   273
\newcommand{\Evld}[1]{\mathop{\vld}\nolimits_{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   274
\newcommand{\notEvld}[1]{\mathop{\not\vld}\nolimits_{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   275
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   276
\newcommand{\EQ}{\fct{EQ}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   277
\newcommand{\IMPL}{\fct{IMPL}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   278
\newcommand{\ALL}{\fct{ALL}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   279
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   280
\newcommand{\extcv}{\mathrel{\unlhd}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   281
\newcommand{\weakth}{\preceq}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   282
\newcommand{\eqvth}{\approx}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   283
\newcommand{\extdcli}{\mathrel{<_{\rm dcl}^1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   284
\newcommand{\extdcl}{\mathrel{\le_{\rm dcl}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   285
\newcommand{\extdfni}{\mathrel{<_{\rm dfn}^1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   286
\newcommand{\extdfn}{\mathrel{\le_{\rm dfn}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   287
\newcommand{\extsdfn}{\mathrel{\le_{\rm sdfn}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   288
\newcommand{\extqdfn}{\mathrel{\le_{\rm qdfn}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   289
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   290
\newcommand{\lvarbl}{\langle}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   291
\newcommand{\rvarbl}{\rangle}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   292
\newcommand{\varbl}[1]{{\lvarbl #1\rvarbl}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   293
\newcommand{\up}{{\scriptstyle\mathord\uparrow}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   294
\newcommand{\down}{{\scriptstyle\mathord\downarrow}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   295
\newcommand{\Down}{{\mathord\downarrow}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   296
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   297
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   298
\newcommand{\Sle}{{\mathrel{\le_S}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   299
\newcommand{\Classes}{\syn{Classes}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   300
\newcommand{\ClassNames}{\syn{ClassNames}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   301
\newcommand{\Sorts}{\syn{Sorts}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   302
\newcommand{\TyVarNames}{\syn{TyVarNames}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   303
\newcommand{\STyVars}{\syn{STyVars}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   304
\newcommand{\STyArities}{\syn{STyArities}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   305
\newcommand{\STypes}{\syn{STypes}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   306
\newcommand{\SVars}{\syn{SVars}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   307
\newcommand{\SConsts}{\syn{SConsts}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   308
\newcommand{\STerms}{\syn{STerms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   309
\newcommand{\SForms}{\syn{SForms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   310
\newcommand{\SAxms}{\syn{SAxms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   311
\newcommand{\T}{{\cal T}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   312
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   313
\newcommand{\cls}[1]{{\mathord{\sl #1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   314
\newcommand{\intsrt}{\sqcap}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   315
\newcommand{\Intsrt}{{\mathop\sqcap}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   316
\newcommand{\subcls}{\preceq}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   317
\newcommand{\Subcls}[1]{\mathrel{\subcls_{#1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   318
\newcommand{\subsrt}{\sqsubseteq}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   319
\newcommand{\Subsrt}[1]{\mathrel{\subsrt_{#1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   320
\newcommand{\subsrtp}{\sqsubset}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   321
\newcommand{\eqvsrt}{\approx}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   322
\newcommand{\topsrt}{\top}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   323
\newcommand{\srt}{\ty}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   324
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   325
\newcommand{\sct}[1]{{\bf #1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   326
\newcommand{\CLASSES}{\sct{classes}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   327
\newcommand{\CLASSREL}{\sct{classrel}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   328
\newcommand{\TYPES}{\sct{types}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   329
\newcommand{\ARITIES}{\sct{arities}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   330
\newcommand{\CONSTS}{\sct{consts}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   331
\newcommand{\AXIOMS}{\sct{axioms}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   332
\newcommand{\DEFNS}{\sct{defns}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   333
\newcommand{\AXCLASS}{\sct{axclass}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   334
\newcommand{\INSTANCE}{\sct{instance}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   335
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   336
\newcommand{\Srt}{{\mathbin{\,:\,}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   337
\newcommand{\insrt}[2]{{\mathopen{(\!|} #1 \Srt #2 \mathclose{|\!)}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   338
\newcommand{\ofsrt}[2]{{\mathopen{\langle\!|} #1 \Srt #2 \mathclose{|\!\rangle}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   339
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   340
\newcommand{\injV}{{\iota_V}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   341
\newcommand{\inj}{\iota}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   342
\newcommand{\injC}{{\iota_C}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   343
\newcommand{\I}{{\cal I}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   344
\newcommand{\C}{{\cal C}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   345
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   346
\newcommand{\Sdrv}{\mathrel{\vdash\!\!\!\vdash}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   347
\newcommand{\SDrv}[1]{\mathrel{\mathord{\Sdrv}_{#1}}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   348
\newcommand{\SGdrv}{\Gam\Sdrv}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   349
\newcommand{\Sedrv}{\mathop{\Sdrv}\nolimits}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   350
\newcommand{\SEdrv}[1]{\mathop{\Sdrv}\nolimits_{#1}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   351
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   352
\newcommand{\SSubclass}{\rmtext{S-Subclass}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   353
\newcommand{\SSubsort}{\rmtext{S-Subsort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   354
\newcommand{\SVarSort}{\rmtext{S-VarSort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   355
\newcommand{\SArity}{\rmtext{S-Arity}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   356
\newcommand{\SSortMP}{\rmtext{S-SortMP}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   357
\newcommand{\STopSort}{\rmtext{S-TopSort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   358
\newcommand{\SOfSort}{\rmtext{S-OfSort}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   359
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   360
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   361
\makeatother
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   362