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