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;
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@22317
     6
\usepackage{listings}
haftmann@20946
     7
\usepackage[refpage]{nomencl}
haftmann@20946
     8
\usepackage{../../iman,../../extra,../../isar,../../proof}
wenzelm@26911
     9
\usepackage{../../isabelle,../../isabellesym}
haftmann@20946
    10
\usepackage{style}
wenzelm@26911
    11
\usepackage{../../pdfsetup}
haftmann@20946
    12
haftmann@22347
    13
\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
haftmann@22347
    14
\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
haftmann@22347
    15
\renewcommand{\isasymotimes}{\isamath{\circ}}
haftmann@22347
    16
haftmann@20946
    17
\newcommand{\cmd}[1]{\isacommand{#1}}
haftmann@20946
    18
haftmann@20946
    19
\newcommand{\isasymINFIX}{\cmd{infix}}
haftmann@20946
    20
\newcommand{\isasymLOCALE}{\cmd{locale}}
haftmann@20946
    21
\newcommand{\isasymINCLUDES}{\cmd{includes}}
haftmann@20946
    22
\newcommand{\isasymDATATYPE}{\cmd{datatype}}
haftmann@20946
    23
\newcommand{\isasymAXCLASS}{\cmd{axclass}}
haftmann@20946
    24
\newcommand{\isasymFIXES}{\cmd{fixes}}
haftmann@20946
    25
\newcommand{\isasymASSUMES}{\cmd{assumes}}
haftmann@20946
    26
\newcommand{\isasymDEFINES}{\cmd{defines}}
haftmann@20946
    27
\newcommand{\isasymNOTES}{\cmd{notes}}
haftmann@20946
    28
\newcommand{\isasymSHOWS}{\cmd{shows}}
haftmann@20946
    29
\newcommand{\isasymCLASS}{\cmd{class}}
haftmann@20946
    30
\newcommand{\isasymINSTANCE}{\cmd{instance}}
haftmann@25533
    31
\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
haftmann@25871
    32
\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
haftmann@20946
    33
\newcommand{\isasymLEMMA}{\cmd{lemma}}
haftmann@20946
    34
\newcommand{\isasymPROOF}{\cmd{proof}}
haftmann@20946
    35
\newcommand{\isasymQED}{\cmd{qed}}
haftmann@20946
    36
\newcommand{\isasymFIX}{\cmd{fix}}
haftmann@20946
    37
\newcommand{\isasymASSUME}{\cmd{assume}}
haftmann@20946
    38
\newcommand{\isasymSHOW}{\cmd{show}}
haftmann@20946
    39
\newcommand{\isasymNOTE}{\cmd{note}}
haftmann@20946
    40
haftmann@20946
    41
\newcommand{\qt}[1]{``#1''}
haftmann@20946
    42
\newcommand{\qtt}[1]{"{}{#1}"{}}
haftmann@20946
    43
\newcommand{\qn}[1]{\emph{#1}}
haftmann@20946
    44
\newcommand{\strong}[1]{{\bfseries #1}}
haftmann@20946
    45
\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
haftmann@20946
    46
haftmann@22317
    47
\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
haftmann@22317
    48
\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
haftmann@22317
    49
\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
haftmann@22317
    50
haftmann@20946
    51
\hyphenation{Isabelle}
haftmann@20946
    52
\hyphenation{Isar}
haftmann@20946
    53
haftmann@20946
    54
\isadroptag{theory}
haftmann@20946
    55
\title{\includegraphics[scale=0.5]{isabelle_isar}
haftmann@20946
    56
  \\[4ex] Haskell-style type classes with Isabelle/Isar}
haftmann@20946
    57
\author{\emph{Florian Haftmann}}
haftmann@20946
    58
haftmann@20946
    59
haftmann@20946
    60
\begin{document}
haftmann@20946
    61
haftmann@20946
    62
\maketitle
haftmann@20946
    63
haftmann@20946
    64
\begin{abstract}
haftmann@20946
    65
  This tutorial introduces the look-and-feel of Isar type classes
haftmann@20946
    66
  to the end-user; Isar type classes are a convenient mechanism
haftmann@20946
    67
  for organizing specifications, overcoming some drawbacks
haftmann@20946
    68
  of raw axiomatic type classes. Essentially, they combine
haftmann@20946
    69
  an operational aspect (in the manner of Haskell) with
haftmann@20946
    70
  a logical aspect, both managed uniformly.
haftmann@20946
    71
\end{abstract}
haftmann@20946
    72
haftmann@20946
    73
\thispagestyle{empty}\clearpage
haftmann@20946
    74
haftmann@20946
    75
\pagenumbering{roman}
haftmann@20946
    76
\clearfirst
haftmann@20946
    77
haftmann@20946
    78
\input{Thy/document/Classes.tex}
haftmann@20946
    79
haftmann@20946
    80
\begingroup
haftmann@20946
    81
%\tocentry{\bibname}
haftmann@20946
    82
\bibliographystyle{plain} \small\raggedright\frenchspacing
haftmann@23956
    83
\bibliography{../../manual}
haftmann@20946
    84
\endgroup
haftmann@20946
    85
haftmann@20946
    86
\end{document}
haftmann@20946
    87
haftmann@20946
    88
haftmann@20946
    89
%%% Local Variables: 
haftmann@20946
    90
%%% mode: latex
haftmann@20946
    91
%%% TeX-master: t
haftmann@20946
    92
%%% End: