--- a/CookBook/document/root.tex	Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/document/root.tex	Wed Jan 14 23:44:14 2009 +0000
@@ -35,7 +35,7 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % sane default for proof documents
-\parindent 0pt\parskip 0.7ex
+\parindent 0pt\parskip 0.6ex
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \hyphenation{Isabelle}
@@ -59,7 +59,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this is to draw a gray box around code
 \makeatletter\newenvironment{graybox}{%
-  \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
+  \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}%
   \colorbox{gray!10}{\usebox{\@tempboxa}}
 }\makeatother
 
@@ -72,19 +72,22 @@
 \renewcommand{\isacharverbatimclose}{}}{}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% for code
 \isakeeptag{CookBookML}
-\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
-\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip}
+\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{isabelle}\begin{graybox}}
+\renewcommand{\endisatagCookBookML}{\end{graybox}\end{isabelle}\end{vanishML}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% for line numbers
+% for code that has line numbers
 \isakeeptag{linenumbers}
 \renewcommand{\isataglinenumbers}
-{\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
-\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip}
+{\begin{vanishML}\begin{isabelle}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
+\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{isabelle}\end{vanishML}}
 
-
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\small\item\relax}
+{\end{isabellebody}\end{trivlist}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}