src/Doc/Classes/document/root.tex
author haftmann
Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734 89347c0cc6a3
parent 78682 46891e209d72
permissions -rw-r--r--
treat map_filter similar to list_all, list_ex, list_ex1
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}
78682
46891e209d72 proper fontenc for cartouches (amending d052d61da398);
wenzelm
parents: 73723
diff changeset
     2
\usepackage[T1]{fontenc}
73401
8b464825d2b5 removed unused latex packages;
wenzelm
parents: 50426
diff changeset
     3
\usepackage{graphicx}
50426
d2c60ada3ece eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
wenzelm
parents: 48985
diff changeset
     4
\usepackage{iman,extra,isar}
48950
9965099f51ad more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
     5
\usepackage{isabelle,isabellesym}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     6
\usepackage{style}
48950
9965099f51ad more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
     7
\usepackage{pdfsetup}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     8
75b56e51fade initial draft
haftmann
parents:
diff changeset
     9
75b56e51fade initial draft
haftmann
parents:
diff changeset
    10
\hyphenation{Isabelle}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    11
\hyphenation{Isar}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    12
\isadroptag{theory}
28565
haftmann
parents: 28540
diff changeset
    13
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73401
diff changeset
    14
\title{\includegraphics[scale=0.5]{isabelle_logo}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    15
  \\[4ex] Haskell-style type classes with Isabelle/Isar}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    16
\author{\emph{Florian Haftmann}}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    17
75b56e51fade initial draft
haftmann
parents:
diff changeset
    18
\begin{document}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    19
75b56e51fade initial draft
haftmann
parents:
diff changeset
    20
\maketitle
75b56e51fade initial draft
haftmann
parents:
diff changeset
    21
75b56e51fade initial draft
haftmann
parents:
diff changeset
    22
\begin{abstract}
31691
7d50527dc008 Polishing the English
paulson
parents: 31256
diff changeset
    23
  \noindent This tutorial introduces Isar type classes, which 
31256
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    24
  are a convenient mechanism for organizing specifications.
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    25
  Essentially, they combine an operational aspect (in the
cf75908fd3c3 weakend references to old axclass
haftmann
parents: 30227
diff changeset
    26
  manner of Haskell) with a logical aspect, both managed uniformly.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    27
\end{abstract}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    28
75b56e51fade initial draft
haftmann
parents:
diff changeset
    29
\thispagestyle{empty}\clearpage
75b56e51fade initial draft
haftmann
parents:
diff changeset
    30
75b56e51fade initial draft
haftmann
parents:
diff changeset
    31
\pagenumbering{roman}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    32
\clearfirst
75b56e51fade initial draft
haftmann
parents:
diff changeset
    33
48950
9965099f51ad more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
    34
\input{Classes.tex}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    35
75b56e51fade initial draft
haftmann
parents:
diff changeset
    36
\begingroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    37
\bibliographystyle{plain} \small\raggedright\frenchspacing
48950
9965099f51ad more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
    38
\bibliography{manual}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    39
\endgroup
75b56e51fade initial draft
haftmann
parents:
diff changeset
    40
75b56e51fade initial draft
haftmann
parents:
diff changeset
    41
\end{document}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    42
75b56e51fade initial draft
haftmann
parents:
diff changeset
    43
75b56e51fade initial draft
haftmann
parents:
diff changeset
    44
%%% Local Variables: 
75b56e51fade initial draft
haftmann
parents:
diff changeset
    45
%%% mode: latex
75b56e51fade initial draft
haftmann
parents:
diff changeset
    46
%%% TeX-master: t
75b56e51fade initial draft
haftmann
parents:
diff changeset
    47
%%% End: