doc-src/Classes/classes.tex
author wenzelm
Sun, 01 May 2011 16:36:34 +0200
changeset 42511 bf89455ccf9d
parent 31691 7d50527dc008
permissions -rw-r--r--
eliminated copies of isabelle style files;
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}
42511
bf89455ccf9d eliminated copies of isabelle style files;
wenzelm
parents: 31691
diff changeset
     6
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/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}
31691
7d50527dc008 Polishing the English
paulson
parents: 31256
diff changeset
    24
  \noindent This tutorial introduces Isar type classes, which 
31256
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    25
  are a convenient mechanism for organizing specifications.
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    26
  Essentially, they combine an operational aspect (in the
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    27
  manner of Haskell) with a logical aspect, both managed uniformly.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    28
\end{abstract}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    29
75b56e51fade initial draft
haftmann
parents:
diff changeset
    30
\thispagestyle{empty}\clearpage
75b56e51fade initial draft
haftmann
parents:
diff changeset
    31
75b56e51fade initial draft
haftmann
parents:
diff changeset
    32
\pagenumbering{roman}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    33
\clearfirst
75b56e51fade initial draft
haftmann
parents:
diff changeset
    34
75b56e51fade initial draft
haftmann
parents:
diff changeset
    35
\input{Thy/document/Classes.tex}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    36
75b56e51fade initial draft
haftmann
parents:
diff changeset
    37
\begingroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    38
\bibliographystyle{plain} \small\raggedright\frenchspacing
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29016
diff changeset
    39
\bibliography{../manual}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    40
\endgroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    41
75b56e51fade initial draft
haftmann
parents:
diff changeset
    42
\end{document}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    43
75b56e51fade initial draft
haftmann
parents:
diff changeset
    44
75b56e51fade initial draft
haftmann
parents:
diff changeset
    45
%%% Local Variables: 
75b56e51fade initial draft
haftmann
parents:
diff changeset
    46
%%% mode: latex
75b56e51fade initial draft
haftmann
parents:
diff changeset
    47
%%% TeX-master: t
75b56e51fade initial draft
haftmann
parents:
diff changeset
    48
%%% End: