doc-src/IsarAdvanced/Classes/classes.tex
author haftmann
Mon Nov 03 14:15:25 2008 +0100 (2008-11-03)
changeset 28714 1992553cccfe
parent 28565 519b17118926
child 28727 185110a4b97a
permissions -rw-r--r--
improved verbatim mechanism
     1 
     2 %% $Id$
     3 
     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}
    11 
    12 
    13 %% setup
    14 
    15 % hyphenation
    16 \hyphenation{Isabelle}
    17 \hyphenation{Isar}
    18 
    19 % logical markup
    20 \newcommand{\strong}[1]{{\bfseries {#1}}}
    21 \newcommand{\qn}[1]{\emph{#1}}
    22 
    23 % typographic conventions
    24 \newcommand{\qt}[1]{``{#1}''}
    25 
    26 % verbatim text
    27 \newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    28 
    29 % invisibility
    30 \isadroptag{theory}
    31 
    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
    39 
    40 %\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
    41 %\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
    42 %\renewcommand{\isasymotimes}{\isamath{\circ}}
    43 
    44 
    45 %% content
    46 
    47 \title{\includegraphics[scale=0.5]{isabelle_isar}
    48   \\[4ex] Haskell-style type classes with Isabelle/Isar}
    49 \author{\emph{Florian Haftmann}}
    50 
    51 \begin{document}
    52 
    53 \maketitle
    54 
    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}
    63 
    64 \thispagestyle{empty}\clearpage
    65 
    66 \pagenumbering{roman}
    67 \clearfirst
    68 
    69 \input{Thy/document/Classes.tex}
    70 
    71 \begingroup
    72 %\tocentry{\bibname}
    73 \bibliographystyle{plain} \small\raggedright\frenchspacing
    74 \bibliography{../../manual}
    75 \endgroup
    76 
    77 \end{document}
    78 
    79 
    80 %%% Local Variables: 
    81 %%% mode: latex
    82 %%% TeX-master: t
    83 %%% End: