# HG changeset patch
# User haftmann
# Date 1228727690 -3600
# Node ID 31110b40eae76e5f5048afb6c7fee71b6f4e0315
# Parent  4546ccf7294277de9d0c1f8aa53fdbf3a756d269
tuned LaTeX files

diff -r 4546ccf72942 -r 31110b40eae7 doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Sat Dec 06 23:19:44 2008 -0800
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon Dec 08 10:14:50 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
 
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx}
@@ -10,40 +8,10 @@
 \usepackage{../../pdfsetup}
 
 
-%% setup
-
-% 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{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
-% 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}}
@@ -69,7 +37,6 @@
 \input{Thy/document/Classes.tex}
 
 \begingroup
-%\tocentry{\bibname}
 \bibliographystyle{plain} \small\raggedright\frenchspacing
 \bibliography{../../manual}
 \endgroup
diff -r 4546ccf72942 -r 31110b40eae7 doc-src/IsarAdvanced/Classes/style.sty
--- a/doc-src/IsarAdvanced/Classes/style.sty	Sat Dec 06 23:19:44 2008 -0800
+++ b/doc-src/IsarAdvanced/Classes/style.sty	Mon Dec 08 10:14:50 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
 
 %% toc
 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
@@ -7,54 +5,37 @@
 
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
-%% glossary
-\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
-\newcommand{\seeglossary}[1]{\emph{#1}}
-\newcommand{\glossaryname}{Glossary}
-\renewcommand{\nomname}{\glossaryname}
-\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+%% verbatim text
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
-\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
-\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
-\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
+%% 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
 
-%% math
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\isasymvartheta}{\isamath{\theta}}
-\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
-
+%% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 \pagestyle{headings}
-\sloppy
 \binperiod
 \underscoreon
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
-
-\isafoldtag{FIXME}
-\isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
-\renewcommand{\endisatagmlref}{\endgroup}
+\isabellestyle{it}
 
-\newcommand{\isasymGUESS}{\isakeyword{guess}}
-\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
-\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymEND}{\isakeyword{end}}
-\newcommand{\isasymCONSTS}{\isakeyword{consts}}
-\newcommand{\isasymDEFS}{\isakeyword{defs}}
-\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
-\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
-
-\isabellestyle{it}
 
 %%% Local Variables: 
 %%% mode: latex