--- a/CookBook/document/root.tex	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/document/root.tex	Thu Oct 30 13:36:51 2008 +0100
@@ -9,8 +9,16 @@
 \usepackage{rail}
 \usepackage{url}
 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
+\usepackage{pdfsetup}
 
-% Cross references to other manuals:
+\urlstyle{rm}
+\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
+\renewcommand{\isastyleminor}{\tt\slshape}%
+\renewcommand{\isastyle}{\small\tt\slshape}%
+\isadroptag{theory}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% For cross references to the other manuals:
 \usepackage{xr}
 \externaldocument[I-]{implementation}
 \newcommand{\impref}[1]{\ref{I-#1}}
@@ -21,41 +29,54 @@
 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
 
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
-\renewcommand{\isastyleminor}{\tt\slshape}%
-\renewcommand{\isastyle}{\small\tt\slshape}%
-\isadroptag{theory}
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % sane default for proof documents
 \parindent 0pt\parskip 0.6ex
 
-% for comments on the margin
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% 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}.}}
+
 \newcommand{\readmoremarginpar}[1]%
 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
 
 \newenvironment{readmore}%
 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
 
-% to work around a problem with \isanewline
-\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
-
-\renewenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\small\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-% for exercises and comments
-\newtheorem{exercise}{Exercise}[section]
-\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% 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}}
+\newenvironment{mytable}
+{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}
+{\end{tabular}\end{trivlist}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \hyphenation{Isabelle}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% this hack is for getting rid of the ML {* ... *} 
+% scaffolding around function definitions
+\newenvironment{vanishML}{%
+\renewcommand{\isacommand}[1]{}%
+\renewcommand{\isacharverbatimopen}{}%
+\renewcommand{\isacharverbatimclose}{}%
+\hspace{-1.5mm}\mbox{}}{}
+
+\renewcommand{\isatagML}{\begin{vanishML}}
+\renewcommand{\endisatagML}{\end{vanishML}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{document}
 
 \title{\mbox{}\\[-10ex]
@@ -71,7 +92,6 @@
 
 \tableofcontents
 
-
 % generated text of all theories
 \input{session}