diff -r bbb2d5f1d58d -r 14c3dd5ee2ad CookBook/document/root.tex
--- a/CookBook/document/root.tex	Wed Jan 14 18:30:41 2009 +0000
+++ b/CookBook/document/root.tex	Wed Jan 14 21:46:04 2009 +0000
@@ -21,7 +21,7 @@
 \renewcommand{\isastyle}{\small\tt\slshape}%
 \isadroptag{theory}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For cross references to the other manuals:
 \usepackage{xr}
 \externaldocument[I-]{implementation}
@@ -33,21 +33,18 @@
 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % sane default for proof documents
-\parindent 0pt\parskip 0.6ex
+\parindent 0pt\parskip 0.7ex
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\hyphenation{Isabelle}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % to work around a problem with \isanewline
 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% FIXME: WHAT DOES THIS DO?
-\renewenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\small\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for exercises, comments and readmores
 \newtheorem{exercise}{Exercise}[section]
 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
@@ -58,17 +55,15 @@
 \newenvironment{readmore}%
 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% FIXME: THIS SHOULD NOT BE USED ANYMORE
-% a table environment with proper indentation
-\newenvironment{mytable}
-{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}
-{\end{tabular}\end{trivlist}}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\hyphenation{Isabelle}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% this is to draw a gray box around code
+\makeatletter\newenvironment{graybox}{%
+  \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
+  \colorbox{gray!10}{\usebox{\@tempboxa}}
+}\makeatother
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this hack is for getting rid of the ML {* ... *} 
 % scaffolding around function definitions
 \newenvironment{vanishML}{%
@@ -76,31 +71,27 @@
 \renewcommand{\isacharverbatimopen}{}%
 \renewcommand{\isacharverbatimclose}{}}{}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\makeatletter\newenvironment{graybox}{%
-   \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
-   \colorbox{gray!5}{\usebox{\@tempboxa}}
-}\makeatother
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \isakeeptag{CookBookML}
 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for line numbers
 \isakeeptag{linenumbers}
 \renewcommand{\isataglinenumbers}
 {\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
 
 \title{\mbox{}\\[-10ex]
        \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
        The Isabelle Programmer's Cookbook (fragment)}
+
 \author{with contributions by:\\[2ex] 
         \begin{tabular}{r@{\hspace{1.8mm}}l}
         Stefan & Berghofer\\
@@ -108,8 +99,8 @@
         Jeremy & Dawson\\
         Alexander & Krauss\\ 
         \end{tabular}}
+
 \maketitle
-
 \tableofcontents
 
 % generated text of all theories