doc-src/IsarAdvanced/Classes/classes.tex
author nipkow
Sun, 22 Feb 2009 17:25:28 +0100
changeset 30056 0a35bee25c20
parent 29016 31110b40eae7
permissions -rw-r--r--
added lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     1
75b56e51fade initial draft
haftmann
parents:
diff changeset
     2
\documentclass[12pt,a4paper,fleqn]{report}
75b56e51fade initial draft
haftmann
parents:
diff changeset
     3
\usepackage{latexsym,graphicx}
75b56e51fade initial draft
haftmann
parents:
diff changeset
     4
\usepackage[refpage]{nomencl}
75b56e51fade initial draft
haftmann
parents:
diff changeset
     5
\usepackage{../../iman,../../extra,../../isar,../../proof}
26911
871cc7f11034 use Isabelle sty files from Doc/;
wenzelm
parents: 26784
diff changeset
     6
\usepackage{../../isabelle,../../isabellesym}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     7
\usepackage{style}
26911
871cc7f11034 use Isabelle sty files from Doc/;
wenzelm
parents: 26784
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}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    24
  This tutorial introduces the look-and-feel of Isar type classes
75b56e51fade initial draft
haftmann
parents:
diff changeset
    25
  to the end-user; Isar type classes are a convenient mechanism
75b56e51fade initial draft
haftmann
parents:
diff changeset
    26
  for organizing specifications, overcoming some drawbacks
75b56e51fade initial draft
haftmann
parents:
diff changeset
    27
  of raw axiomatic type classes. Essentially, they combine
75b56e51fade initial draft
haftmann
parents:
diff changeset
    28
  an operational aspect (in the manner of Haskell) with
75b56e51fade initial draft
haftmann
parents:
diff changeset
    29
  a logical aspect, both managed uniformly.
75b56e51fade initial draft
haftmann
parents:
diff changeset
    30
\end{abstract}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    31
75b56e51fade initial draft
haftmann
parents:
diff changeset
    32
\thispagestyle{empty}\clearpage
75b56e51fade initial draft
haftmann
parents:
diff changeset
    33
75b56e51fade initial draft
haftmann
parents:
diff changeset
    34
\pagenumbering{roman}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    35
\clearfirst
75b56e51fade initial draft
haftmann
parents:
diff changeset
    36
75b56e51fade initial draft
haftmann
parents:
diff changeset
    37
\input{Thy/document/Classes.tex}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    38
75b56e51fade initial draft
haftmann
parents:
diff changeset
    39
\begingroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    40
\bibliographystyle{plain} \small\raggedright\frenchspacing
23956
48494ccfabaf updated
haftmann
parents: 22347
diff changeset
    41
\bibliography{../../manual}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    42
\endgroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    43
75b56e51fade initial draft
haftmann
parents:
diff changeset
    44
\end{document}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    45
75b56e51fade initial draft
haftmann
parents:
diff changeset
    46
75b56e51fade initial draft
haftmann
parents:
diff changeset
    47
%%% Local Variables: 
75b56e51fade initial draft
haftmann
parents:
diff changeset
    48
%%% mode: latex
75b56e51fade initial draft
haftmann
parents:
diff changeset
    49
%%% TeX-master: t
75b56e51fade initial draft
haftmann
parents:
diff changeset
    50
%%% End: