author wenzelm Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago) changeset 28500 4b79e5d3d0aa parent 26911 871cc7f11034 child 28540 541366e3c1b3 permissions -rw-r--r--
replaced ISATOOL by ISABELLE_TOOL;
     1

     2 %% $Id$

     3

     4 \documentclass[12pt,a4paper,fleqn]{report}

     5 \usepackage{latexsym,graphicx}

     6 \usepackage{listings}

     7 \usepackage[refpage]{nomencl}

     8 \usepackage{../../iman,../../extra,../../isar,../../proof}

     9 \usepackage{../../isabelle,../../isabellesym}

    10 \usepackage{style}

    11 \usepackage{../../pdfsetup}

    12

    13 \renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}

    14 \renewcommand{\isasymdiv}{\isamath{{}^{-1}}}

    15 \renewcommand{\isasymotimes}{\isamath{\circ}}

    16

    17 \newcommand{\cmd}[1]{\isacommand{#1}}

    18

    19 \newcommand{\isasymINFIX}{\cmd{infix}}

    20 \newcommand{\isasymLOCALE}{\cmd{locale}}

    21 \newcommand{\isasymINCLUDES}{\cmd{includes}}

    22 \newcommand{\isasymDATATYPE}{\cmd{datatype}}

    23 \newcommand{\isasymAXCLASS}{\cmd{axclass}}

    24 \newcommand{\isasymFIXES}{\cmd{fixes}}

    25 \newcommand{\isasymASSUMES}{\cmd{assumes}}

    26 \newcommand{\isasymDEFINES}{\cmd{defines}}

    27 \newcommand{\isasymNOTES}{\cmd{notes}}

    28 \newcommand{\isasymSHOWS}{\cmd{shows}}

    29 \newcommand{\isasymCLASS}{\cmd{class}}

    30 \newcommand{\isasymINSTANCE}{\cmd{instance}}

    31 \newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}

    32 \newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}

    33 \newcommand{\isasymLEMMA}{\cmd{lemma}}

    34 \newcommand{\isasymPROOF}{\cmd{proof}}

    35 \newcommand{\isasymQED}{\cmd{qed}}

    36 \newcommand{\isasymFIX}{\cmd{fix}}

    37 \newcommand{\isasymASSUME}{\cmd{assume}}

    38 \newcommand{\isasymSHOW}{\cmd{show}}

    39 \newcommand{\isasymNOTE}{\cmd{note}}

    40

    41 \newcommand{\qt}[1]{#1''}

    42 \newcommand{\qtt}[1]{"{}{#1}"{}}

    43 \newcommand{\qn}[1]{\emph{#1}}

    44 \newcommand{\strong}[1]{{\bfseries #1}}

    45 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}}

    46

    47 \lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}

    48 \newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}

    49 \newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}

    50

    51 \hyphenation{Isabelle}

    52 \hyphenation{Isar}

    53

    54 \isadroptag{theory}

    55 \title{\includegraphics[scale=0.5]{isabelle_isar}

    56   \\[4ex] Haskell-style type classes with Isabelle/Isar}

    57 \author{\emph{Florian Haftmann}}

    58

    59

    60 \begin{document}

    61

    62 \maketitle

    63

    64 \begin{abstract}

    65   This tutorial introduces the look-and-feel of Isar type classes

    66   to the end-user; Isar type classes are a convenient mechanism

    67   for organizing specifications, overcoming some drawbacks

    68   of raw axiomatic type classes. Essentially, they combine

    69   an operational aspect (in the manner of Haskell) with

    70   a logical aspect, both managed uniformly.

    71 \end{abstract}

    72

    73 \thispagestyle{empty}\clearpage

    74

    75 \pagenumbering{roman}

    76 \clearfirst

    77

    78 \input{Thy/document/Classes.tex}

    79

    80 \begingroup

    81 %\tocentry{\bibname}

    82 \bibliographystyle{plain} \small\raggedright\frenchspacing

    83 \bibliography{../../manual}

    84 \endgroup

    85

    86 \end{document}

    87

    88

    89 %%% Local Variables:

    90 %%% mode: latex

    91 %%% TeX-master: t

    92 %%% End: