# HG changeset patch
# User nipkow
# Date 1319725714 -7200
# Node ID 85b0ca9dd82fa07c4d6213146adb34150360ac8d
# Parent  cd0f6643e9982ced7f58b2b59b14f294e05a7a73
uses IMP and hence requires its tex setup

diff -r cd0f6643e998 -r 85b0ca9dd82f src/HOL/HOLCF/IMP/document/isaverbatimwrite.sty
--- /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}
diff -r cd0f6643e998 -r 85b0ca9dd82f src/HOL/HOLCF/IMP/document/root.tex
--- 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}