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