src/Doc/Typeclass_Hierarchy/document/root.tex
author wenzelm
Fri, 19 May 2017 18:10:19 +0200
changeset 65875 12c90c0c4b32
parent 63026 9a9c2d846d4a
child 73723 1bbbaae6b5e3
permissions -rw-r--r--
suppress ANSI control sequences in Scala console;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63026
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     1
\documentclass[12pt,a4paper,fleqn]{article}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     2
\usepackage{latexsym,graphicx}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     3
\usepackage{iman,extra,isar}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     5
\usepackage{style}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     6
\usepackage{pdfsetup}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     7
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     8
\hyphenation{Isabelle}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
     9
\hyphenation{Isar}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    10
\isadroptag{theory}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    11
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    12
\title{\includegraphics[scale=0.5]{isabelle_isar}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    13
  \\[4ex] The {Isabelle/HOL} type-class hierarchy}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    14
\author{\emph{Florian Haftmann}}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    15
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    16
\begin{document}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    17
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    18
\maketitle
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    19
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    20
\begin{abstract}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    21
  \noindent This primer introduces corner stones of the {Isabelle/HOL}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    22
  type-class hierarchy and gives some insights into its internal
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    23
  organization.
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    24
\end{abstract}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    25
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    26
\thispagestyle{empty}\clearpage
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    27
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    28
\pagenumbering{roman}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    29
\clearfirst
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    30
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    31
\input{Typeclass_Hierarchy.tex}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    32
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    33
\begingroup
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    34
\bibliographystyle{plain} \small\raggedright\frenchspacing
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    35
\bibliography{manual}
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    36
\endgroup
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    37
9a9c2d846d4a fragment of a HOL type class primer
haftmann
parents:
diff changeset
    38
\end{document}