doc-src/Classes/classes.tex
author haftmann
Tue, 26 May 2009 13:40:50 +0200
changeset 31256 cf75908fd3c3
parent 30227 853abb4853cc
child 31691 7d50527dc008
permissions -rw-r--r--
weakend references to old axclass
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     1
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
     2
\documentclass[12pt,a4paper,fleqn]{article}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     3
\usepackage{latexsym,graphicx}
75b56e51fade initial draft
haftmann
parents:
diff changeset
     4
\usepackage[refpage]{nomencl}
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29016
diff changeset
     5
\usepackage{../iman,../extra,../isar,../proof}
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29016
diff changeset
     6
\usepackage{../isabelle,../isabellesym}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     7
\usepackage{style}
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29016
diff changeset
     8
\usepackage{../pdfsetup}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     9
75b56e51fade initial draft
haftmann
parents:
diff changeset
    10
75b56e51fade initial draft
haftmann
parents:
diff changeset
    11
\hyphenation{Isabelle}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    12
\hyphenation{Isar}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    13
\isadroptag{theory}
28565
haftmann
parents: 28540
diff changeset
    14
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    15
\title{\includegraphics[scale=0.5]{isabelle_isar}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    16
  \\[4ex] Haskell-style type classes with Isabelle/Isar}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    17
\author{\emph{Florian Haftmann}}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    18
75b56e51fade initial draft
haftmann
parents:
diff changeset
    19
\begin{document}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    20
75b56e51fade initial draft
haftmann
parents:
diff changeset
    21
\maketitle
75b56e51fade initial draft
haftmann
parents:
diff changeset
    22
75b56e51fade initial draft
haftmann
parents:
diff changeset
    23
\begin{abstract}
31256
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    24
  \noindent This tutorial introduces the look-and-feel of
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    25
  Isar type classes to the end-user.  Isar type classes
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    26
  are a convenient mechanism for organizing specifications.
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    27
  Essentially, they combine an operational aspect (in the
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    28
  manner of Haskell) with a logical aspect, both managed uniformly.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    29
\end{abstract}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    30
75b56e51fade initial draft
haftmann
parents:
diff changeset
    31
\thispagestyle{empty}\clearpage
75b56e51fade initial draft
haftmann
parents:
diff changeset
    32
75b56e51fade initial draft
haftmann
parents:
diff changeset
    33
\pagenumbering{roman}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    34
\clearfirst
75b56e51fade initial draft
haftmann
parents:
diff changeset
    35
75b56e51fade initial draft
haftmann
parents:
diff changeset
    36
\input{Thy/document/Classes.tex}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    37
75b56e51fade initial draft
haftmann
parents:
diff changeset
    38
\begingroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    39
\bibliographystyle{plain} \small\raggedright\frenchspacing
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29016
diff changeset
    40
\bibliography{../manual}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    41
\endgroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    42
75b56e51fade initial draft
haftmann
parents:
diff changeset
    43
\end{document}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    44
75b56e51fade initial draft
haftmann
parents:
diff changeset
    45
75b56e51fade initial draft
haftmann
parents:
diff changeset
    46
%%% Local Variables: 
75b56e51fade initial draft
haftmann
parents:
diff changeset
    47
%%% mode: latex
75b56e51fade initial draft
haftmann
parents:
diff changeset
    48
%%% TeX-master: t
75b56e51fade initial draft
haftmann
parents:
diff changeset
    49
%%% End: