diff -r 419116f1157a -r e23770bc97c8 doc-src/AxClass/axclass.tex
--- 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