1.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Sat Dec 06 23:19:44 2008 -0800
     1.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon Dec 08 10:14:50 2008 +0100
     1.3 @@ -1,5 +1,3 @@
     1.4 -
     1.5 -%% $Id$
     1.6  
     1.7  \documentclass[12pt,a4paper,fleqn]{report}
     1.8  \usepackage{latexsym,graphicx}
     1.9 @@ -10,40 +8,10 @@
    1.10  \usepackage{../../pdfsetup}
    1.11  
    1.12  
    1.13 -%% setup
    1.14 -
    1.15 -% hyphenation
    1.16  \hyphenation{Isabelle}
    1.17  \hyphenation{Isar}
    1.18 -
    1.19 -% logical markup
    1.20 -\newcommand{\strong}[1]{{\bfseries {#1}}}
    1.21 -\newcommand{\qn}[1]{\emph{#1}}
    1.22 -
    1.23 -% typographic conventions
    1.24 -\newcommand{\qt}[1]{``{#1}''}
    1.25 -
    1.26 -% verbatim text
    1.27 -\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    1.28 -
    1.29 -% invisibility
    1.30  \isadroptag{theory}
    1.31  
    1.32 -% quoted segments
    1.33 -\makeatletter
    1.34 -\isakeeptag{quote}
    1.35 -\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    1.36 -\renewcommand{\isatagquote}{\begin{quotesegment}}
    1.37 -\renewcommand{\endisatagquote}{\end{quotesegment}}
    1.38 -\makeatother
    1.39 -
    1.40 -%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
    1.41 -%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
    1.42 -%\renewcommand{\isasymotimes}{\isamath{\circ}}
    1.43 -
    1.44 -
    1.45 -%% content
    1.46 -
    1.47  \title{\includegraphics[scale=0.5]{isabelle_isar}
    1.48    \\[4ex] Haskell-style type classes with Isabelle/Isar}
    1.49  \author{\emph{Florian Haftmann}}
    1.50 @@ -69,7 +37,6 @@
    1.51  \input{Thy/document/Classes.tex}
    1.52  
    1.53  \begingroup
    1.54 -%\tocentry{\bibname}
    1.55  \bibliographystyle{plain} \small\raggedright\frenchspacing
    1.56  \bibliography{../../manual}
    1.57  \endgroup

     2.1 --- a/doc-src/IsarAdvanced/Classes/style.sty	Sat Dec 06 23:19:44 2008 -0800
     2.2 +++ b/doc-src/IsarAdvanced/Classes/style.sty	Mon Dec 08 10:14:50 2008 +0100
     2.3 @@ -1,5 +1,3 @@
     2.4 -
     2.5 -%% $Id$
     2.6  
     2.7  %% toc
     2.8  \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     2.9 @@ -7,54 +5,37 @@
    2.10  
    2.11  %% references
    2.12  \newcommand{\secref}[1]{\S\ref{#1}}
    2.13 -\newcommand{\chref}[1]{chapter~\ref{#1}}
    2.14  \newcommand{\figref}[1]{figure~\ref{#1}}
    2.15  
    2.16 -%% glossary
    2.17 -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
    2.18 -\newcommand{\seeglossary}[1]{\emph{#1}}
    2.19 -\newcommand{\glossaryname}{Glossary}
    2.20 -\renewcommand{\nomname}{\glossaryname}
    2.21 -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
    2.22 +%% logical markup
    2.23 +\newcommand{\strong}[1]{{\bfseries {#1}}}
    2.24 +\newcommand{\qn}[1]{\emph{#1}}
    2.25  
    2.26 -%% index
    2.27 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    2.28 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    2.29 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    2.30 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    2.31 +%% typographic conventions
    2.32 +\newcommand{\qt}[1]{``{#1}''}
    2.33  
    2.34 -%% math
    2.35 -\newcommand{\text}[1]{\mbox{#1}}
    2.36 -\newcommand{\isasymvartheta}{\isamath{\theta}}
    2.37 -\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    2.38 +%% verbatim text
    2.39 +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    2.40  
    2.41 +%% quoted segments
    2.42 +\makeatletter
    2.43 +\isakeeptag{quote}
    2.44 +\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    2.45 +\renewcommand{\isatagquote}{\begin{quotesegment}}
    2.46 +\renewcommand{\endisatagquote}{\end{quotesegment}}
    2.47 +\makeatother
    2.48 +
    2.49 +%% presentation
    2.50  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    2.51  
    2.52  \pagestyle{headings}
    2.53 -\sloppy
    2.54  \binperiod
    2.55  \underscoreon
    2.56  
    2.57  \renewcommand{\isadigit}[1]{\isamath{#1}}
    2.58  
    2.59 -\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    2.60 +\isabellestyle{it}
    2.61  
    2.62 -\isafoldtag{FIXME}
    2.63 -\isakeeptag{mlref}
    2.64 -\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
    2.65 -\renewcommand{\endisatagmlref}{\endgroup}
    2.66 -
    2.67 -\newcommand{\isasymGUESS}{\isakeyword{guess}}
    2.68 -\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    2.69 -\newcommand{\isasymTHEORY}{\isakeyword{theory}}
    2.70 -\newcommand{\isasymUSES}{\isakeyword{uses}}
    2.71 -\newcommand{\isasymEND}{\isakeyword{end}}
    2.72 -\newcommand{\isasymCONSTS}{\isakeyword{consts}}
    2.73 -\newcommand{\isasymDEFS}{\isakeyword{defs}}
    2.74 -\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    2.75 -\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    2.76 -
    2.77 -\isabellestyle{it}
    2.78  
    2.79  %%% Local Variables: 
    2.80  %%% mode: latex