--- a/doc-src/AxClass/axclass.tex Thu Feb 26 08:44:44 2009 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-
-\documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{graphicx,../iman,../extra,../isar}
-\usepackage{../isabelle,../isabellesym}
-\usepackage{../pdfsetup} % last one!
-
-\isabellestyle{it}
-\newcommand{\isasyminv}{\isamath{{}^{-1}}}
-\renewcommand{\isasymzero}{\isamath{0}}
-\renewcommand{\isasymone}{\isamath{1}}
-
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-\hyphenation{Haskell}
-
-\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Using Axiomatic Type Classes in Isabelle}
-\author{\emph{Markus Wenzel} \\ TU M\"unchen}
-
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-\pagestyle{headings}
-\sloppy
-\binperiod %%%treat . like a binary operator
-
-
-\begin{document}
-
-\underscoreoff
-
-\maketitle
-
-\begin{abstract}
- Isabelle offers order-sorted type classes on top of the simple types of
- plain Higher-Order Logic. The resulting type system is similar to that of
- the programming language Haskell. Its interpretation within the logic
- enables further application, though, apart from restricting polymorphism
- syntactically. In particular, the concept of \emph{Axiomatic Type Classes}
- provides a useful light-weight mechanism for hierarchically-structured
- abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
- axiomatic type classes to model basic algebraic structures.
-
- This document describes axiomatic type classes using Isabelle/Isar theories,
- with proofs expressed via Isar proof language elements. The new theory
- format greatly simplifies the arrangement of the overall development, since
- definitions and proofs may be freely intermixed. Users who prefer tactic
- scripts over structured proofs do not need to fall back on separate ML
- scripts, though, but may refer to Isar's tactic emulation commands.
-\end{abstract}
-
-
-\pagenumbering{roman} \tableofcontents \clearfirst
-
-\include{body}
-
-%FIXME
-\nocite{nipkow-types93}
-\nocite{nipkow-sorts93}
-\nocite{Wenzel:1997:TPHOL}
-\nocite{paulson-isa-book}
-\nocite{isabelle-isar-ref}
-\nocite{Wenzel:1999:TPHOL}
-
-\begingroup
- \bibliographystyle{plain} \small\raggedright\frenchspacing
- \bibliography{../manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-% LocalWords: Isabelle FIXME