uses IMP and hence requires its tex setup

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IMP/document/isaverbatimwrite.sty	Thu Oct 27 16:28:34 2011 +0200
@@ -0,0 +1,16 @@
+\@ifundefined{verbatim@processline}{\input verbatim.sty}{}
+
+\newwrite \isaverbatim@out
+\def\openisaverbatimout#1{\immediate\openout \isaverbatim@out #1}
+\def\closeisaverbatimout{\immediate\closeout \isaverbatim@out}
+\def\isaverbatimwrite{%
+  \@bsphack
+  \let\do\@makeother\dospecials
+  \catcode`\^^M\active \catcode`\^^I=12
+  \def\verbatim@processline{%
+    \immediate\write\isaverbatim@out
+      {\the\verbatim@line}}%
+  \verbatim@start}
+
+\def\endisaverbatimwrite{%
+  \@esphack}

--- a/src/HOL/HOLCF/IMP/document/root.tex	Thu Oct 27 15:59:33 2011 +0200
+++ b/src/HOL/HOLCF/IMP/document/root.tex	Thu Oct 27 16:28:34 2011 +0200
@@ -3,6 +3,7 @@
 \usepackage{isabelle,isabellesym}
 \usepackage{textcomp}
 \usepackage{pdfsetup}
+\usepackage{isaverbatimwrite}
 
 \urlstyle{rm}