doc-src/IsarAdvanced/Classes/classes.tex
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: