wneuper/isa: doc-src/IsarAdvanced/Classes/classes.tex@185110a4b97a

     2 %% $Id$

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

     5 \usepackage{latexsym,graphicx}

     6 \usepackage[refpage]{nomencl}

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

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

     9 \usepackage{style}

    10 \usepackage{../../pdfsetup}

    13 %% setup

    15 % hyphenation

    16 \hyphenation{Isabelle}

    17 \hyphenation{Isar}

    19 % logical markup

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

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

    23 % typographic conventions

    24 \newcommand{\qt}[1]{``{#1}''}

    26 % verbatim text

    27 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}

    29 % invisibility

    30 \isadroptag{theory}

    32 % quoted segments

    33 \makeatletter

    34 \isakeeptag{quote}

    35 \newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}

    36 \renewcommand{\isatagquote}{\begin{quotesegment}}

    37 \renewcommand{\endisatagquote}{\end{quotesegment}}

    38 \makeatother

    40 %\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}

    41 %\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}

    42 %\renewcommand{\isasymotimes}{\isamath{\circ}}

    45 %% content

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

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

    49 \author{\emph{Florian Haftmann}}

    51 \begin{document}

    53 \maketitle

    55 \begin{abstract}

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

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

    58   for organizing specifications, overcoming some drawbacks

    59   of raw axiomatic type classes. Essentially, they combine

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

    61   a logical aspect, both managed uniformly.

    62 \end{abstract}

    64 \thispagestyle{empty}\clearpage

    66 \pagenumbering{roman}

    67 \clearfirst

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

    71 \begingroup

    72 %\tocentry{\bibname}

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

    74 \bibliography{../../manual}

    75 \endgroup

    77 \end{document}

    80 %%% Local Variables:

    81 %%% mode: latex

    82 %%% TeX-master: t

    83 %%% End:

author	haftmann
	Mon, 10 Nov 2008 09:03:28 +0100
changeset 28727	185110a4b97a
parent 28714	1992553cccfe
child 29016	31110b40eae7
permissions	-rw-r--r--