diff -r b99fa5fa63fc -r bca83ed1d45a CookBook/document/root.tex
--- a/CookBook/document/root.tex	Sat Jan 24 21:38:52 2009 +0000
+++ b/CookBook/document/root.tex	Mon Jan 26 01:10:21 2009 +0000
@@ -6,13 +6,12 @@
 \usepackage{charter}
 \usepackage[pdftex]{graphicx}
 \usepackage{proof}
-\usepackage{alltt}
 \usepackage{rail}
 \usepackage{url}
 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
 \usepackage{lineno}
-\usepackage{boxedminipage}
 \usepackage{xcolor}
+\usepackage{framed}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
@@ -35,8 +34,10 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % sane default for proof documents
-\parindent 0pt\parskip 0.6ex
-
+\parindent 0pt
+\parskip 0.6ex
+\abovecaptionskip -3mm
+\belowcaptionskip 10mm
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \hyphenation{Isabelle}
 
@@ -55,13 +56,12 @@
 \newenvironment{readmore}%
 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
 
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this is to draw a gray box around code
-\makeatletter\newenvironment{graybox}{%
-  \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}%
-  \colorbox{gray!20}{\usebox{\@tempboxa}}
-}\makeatother
+%(FIXME redefine pagebreak so that it includes a \smallskip)
+\newenvironment{graybox}
+{\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}}
+{\smallskip\endMakeFramed}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this hack is for getting rid of the ML {* ... *} 
@@ -71,18 +71,15 @@
 \renewcommand{\isacharverbatimopen}{}%
 \renewcommand{\isacharverbatimclose}{}}{}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% for code
 \isakeeptag{CookBookML}
-\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{isabelle}\begin{graybox}}
-\renewcommand{\endisatagCookBookML}{\end{graybox}\end{isabelle}\end{vanishML}}
+\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
+\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for code that has line numbers
 \isakeeptag{linenumbers}
-\renewcommand{\isataglinenumbers}
-{\begin{vanishML}\begin{isabelle}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
-\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{isabelle}\end{vanishML}}
+\renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
+\renewcommand{\endisataglinenumbers}{\par\end{graybox}\end{vanishML}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \renewenvironment{isabelle}