diff -r 1358b1ddd915 -r 519b17118926 doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:52:45 2008 +0200
@@ -3,71 +3,51 @@
 
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx}
-\usepackage{listings}
 \usepackage[refpage]{nomencl}
 \usepackage{../../iman,../../extra,../../isar,../../proof}
 \usepackage{../../isabelle,../../isabellesym}
 \usepackage{style}
 \usepackage{../../pdfsetup}
 
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
-
-\makeatletter
-
-\isakeeptag{quoteme}
-\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquoteme}{\begin{quoteme}}
-\renewcommand{\endisatagquoteme}{\end{quoteme}}
-
-\makeatother
-
-\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
-\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
-\renewcommand{\isasymotimes}{\isamath{\circ}}
-
-\newcommand{\cmd}[1]{\isacommand{#1}}
 
-\newcommand{\isasymINFIX}{\cmd{infix}}
-\newcommand{\isasymLOCALE}{\cmd{locale}}
-\newcommand{\isasymINCLUDES}{\cmd{includes}}
-\newcommand{\isasymDATATYPE}{\cmd{datatype}}
-\newcommand{\isasymAXCLASS}{\cmd{axclass}}
-\newcommand{\isasymFIXES}{\cmd{fixes}}
-\newcommand{\isasymASSUMES}{\cmd{assumes}}
-\newcommand{\isasymDEFINES}{\cmd{defines}}
-\newcommand{\isasymNOTES}{\cmd{notes}}
-\newcommand{\isasymSHOWS}{\cmd{shows}}
-\newcommand{\isasymCLASS}{\cmd{class}}
-\newcommand{\isasymINSTANCE}{\cmd{instance}}
-\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
-\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
-\newcommand{\isasymLEMMA}{\cmd{lemma}}
-\newcommand{\isasymPROOF}{\cmd{proof}}
-\newcommand{\isasymQED}{\cmd{qed}}
-\newcommand{\isasymFIX}{\cmd{fix}}
-\newcommand{\isasymASSUME}{\cmd{assume}}
-\newcommand{\isasymSHOW}{\cmd{show}}
-\newcommand{\isasymNOTE}{\cmd{note}}
+%% setup
 
-\newcommand{\qt}[1]{``#1''}
-\newcommand{\qtt}[1]{"{}{#1}"{}}
-\newcommand{\qn}[1]{\emph{#1}}
-\newcommand{\strong}[1]{{\bfseries #1}}
-\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
-
-\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
-\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
-\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
-
+% hyphenation
 \hyphenation{Isabelle}
 \hyphenation{Isar}
 
+% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+% verbatim text
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
+% invisibility
 \isadroptag{theory}
+
+% quoted segments
+\makeatletter
+\isakeeptag{quote}
+\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquote}{\begin{quotesegment}}
+\renewcommand{\endisatagquote}{\end{quotesegment}}
+\makeatother
+
+%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
+%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
+%\renewcommand{\isasymotimes}{\isamath{\circ}}
+
+
+%% content
+
 \title{\includegraphics[scale=0.5]{isabelle_isar}
   \\[4ex] Haskell-style type classes with Isabelle/Isar}
 \author{\emph{Florian Haftmann}}
 
-
 \begin{document}
 
 \maketitle