doc-src/IsarAdvanced/Classes/classes.tex
author haftmann
Fri Oct 10 15:52:45 2008 +0200 (2008-10-10)
changeset 28565 519b17118926
parent 28540 541366e3c1b3
child 28714 1992553cccfe
permissions -rw-r--r--
tuned
haftmann@20946
     1
haftmann@20946
     2
%% $Id$
haftmann@20946
     3
haftmann@20946
     4
\documentclass[12pt,a4paper,fleqn]{report}
haftmann@20946
     5
\usepackage{latexsym,graphicx}
haftmann@20946
     6
\usepackage[refpage]{nomencl}
haftmann@20946
     7
\usepackage{../../iman,../../extra,../../isar,../../proof}
wenzelm@26911
     8
\usepackage{../../isabelle,../../isabellesym}
haftmann@20946
     9
\usepackage{style}
wenzelm@26911
    10
\usepackage{../../pdfsetup}
haftmann@20946
    11
haftmann@20946
    12
haftmann@28565
    13
%% setup
haftmann@20946
    14
haftmann@28565
    15
% hyphenation
haftmann@20946
    16
\hyphenation{Isabelle}
haftmann@20946
    17
\hyphenation{Isar}
haftmann@20946
    18
haftmann@28565
    19
% logical markup
haftmann@28565
    20
\newcommand{\strong}[1]{{\bfseries {#1}}}
haftmann@28565
    21
\newcommand{\qn}[1]{\emph{#1}}
haftmann@28565
    22
haftmann@28565
    23
% typographic conventions
haftmann@28565
    24
\newcommand{\qt}[1]{``{#1}''}
haftmann@28565
    25
haftmann@28565
    26
% verbatim text
haftmann@28565
    27
\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
haftmann@28565
    28
haftmann@28565
    29
% invisibility
haftmann@20946
    30
\isadroptag{theory}
haftmann@28565
    31
haftmann@28565
    32
% quoted segments
haftmann@28565
    33
\makeatletter
haftmann@28565
    34
\isakeeptag{quote}
haftmann@28565
    35
\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
haftmann@28565
    36
\renewcommand{\isatagquote}{\begin{quotesegment}}
haftmann@28565
    37
\renewcommand{\endisatagquote}{\end{quotesegment}}
haftmann@28565
    38
\makeatother
haftmann@28565
    39
haftmann@28565
    40
%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
haftmann@28565
    41
%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
haftmann@28565
    42
%\renewcommand{\isasymotimes}{\isamath{\circ}}
haftmann@28565
    43
haftmann@28565
    44
haftmann@28565
    45
%% content
haftmann@28565
    46
haftmann@20946
    47
\title{\includegraphics[scale=0.5]{isabelle_isar}
haftmann@20946
    48
  \\[4ex] Haskell-style type classes with Isabelle/Isar}
haftmann@20946
    49
\author{\emph{Florian Haftmann}}
haftmann@20946
    50
haftmann@20946
    51
\begin{document}
haftmann@20946
    52
haftmann@20946
    53
\maketitle
haftmann@20946
    54
haftmann@20946
    55
\begin{abstract}
haftmann@20946
    56
  This tutorial introduces the look-and-feel of Isar type classes
haftmann@20946
    57
  to the end-user; Isar type classes are a convenient mechanism
haftmann@20946
    58
  for organizing specifications, overcoming some drawbacks
haftmann@20946
    59
  of raw axiomatic type classes. Essentially, they combine
haftmann@20946
    60
  an operational aspect (in the manner of Haskell) with
haftmann@20946
    61
  a logical aspect, both managed uniformly.
haftmann@20946
    62
\end{abstract}
haftmann@20946
    63
haftmann@20946
    64
\thispagestyle{empty}\clearpage
haftmann@20946
    65
haftmann@20946
    66
\pagenumbering{roman}
haftmann@20946
    67
\clearfirst
haftmann@20946
    68
haftmann@20946
    69
\input{Thy/document/Classes.tex}
haftmann@20946
    70
haftmann@20946
    71
\begingroup
haftmann@20946
    72
%\tocentry{\bibname}
haftmann@20946
    73
\bibliographystyle{plain} \small\raggedright\frenchspacing
haftmann@23956
    74
\bibliography{../../manual}
haftmann@20946
    75
\endgroup
haftmann@20946
    76
haftmann@20946
    77
\end{document}
haftmann@20946
    78
haftmann@20946
    79
haftmann@20946
    80
%%% Local Variables: 
haftmann@20946
    81
%%% mode: latex
haftmann@20946
    82
%%% TeX-master: t
haftmann@20946
    83
%%% End: