doc-src/Classes/classes.tex
author wenzelm
Sun May 01 16:36:34 2011 +0200 (2011-05-01)
changeset 42511 bf89455ccf9d
parent 31691 7d50527dc008
permissions -rw-r--r--
eliminated copies of isabelle style files;
haftmann@20946
     1
haftmann@30227
     2
\documentclass[12pt,a4paper,fleqn]{article}
haftmann@20946
     3
\usepackage{latexsym,graphicx}
haftmann@20946
     4
\usepackage[refpage]{nomencl}
haftmann@30226
     5
\usepackage{../iman,../extra,../isar,../proof}
wenzelm@42511
     6
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
haftmann@20946
     7
\usepackage{style}
haftmann@30226
     8
\usepackage{../pdfsetup}
haftmann@20946
     9
haftmann@20946
    10
haftmann@20946
    11
\hyphenation{Isabelle}
haftmann@20946
    12
\hyphenation{Isar}
haftmann@20946
    13
\isadroptag{theory}
haftmann@28565
    14
haftmann@20946
    15
\title{\includegraphics[scale=0.5]{isabelle_isar}
haftmann@20946
    16
  \\[4ex] Haskell-style type classes with Isabelle/Isar}
haftmann@20946
    17
\author{\emph{Florian Haftmann}}
haftmann@20946
    18
haftmann@20946
    19
\begin{document}
haftmann@20946
    20
haftmann@20946
    21
\maketitle
haftmann@20946
    22
haftmann@20946
    23
\begin{abstract}
paulson@31691
    24
  \noindent This tutorial introduces Isar type classes, which 
haftmann@31256
    25
  are a convenient mechanism for organizing specifications.
haftmann@31256
    26
  Essentially, they combine an operational aspect (in the
haftmann@31256
    27
  manner of Haskell) with a logical aspect, both managed uniformly.
haftmann@20946
    28
\end{abstract}
haftmann@20946
    29
haftmann@20946
    30
\thispagestyle{empty}\clearpage
haftmann@20946
    31
haftmann@20946
    32
\pagenumbering{roman}
haftmann@20946
    33
\clearfirst
haftmann@20946
    34
haftmann@20946
    35
\input{Thy/document/Classes.tex}
haftmann@20946
    36
haftmann@20946
    37
\begingroup
haftmann@20946
    38
\bibliographystyle{plain} \small\raggedright\frenchspacing
haftmann@30226
    39
\bibliography{../manual}
haftmann@20946
    40
\endgroup
haftmann@20946
    41
haftmann@20946
    42
\end{document}
haftmann@20946
    43
haftmann@20946
    44
haftmann@20946
    45
%%% Local Variables: 
haftmann@20946
    46
%%% mode: latex
haftmann@20946
    47
%%% TeX-master: t
haftmann@20946
    48
%%% End: