# HG changeset patch
# User wenzelm
# Date 1234210139 -3600
# Node ID 02086189262581ace4b035800a8151ebeba48766
# Parent  d2597c4f7e5c55aadae971bc57f2fd4d66182229
set quick_and_dirty;

diff -r d2597c4f7e5c -r 020861892625 doc-src/IsarRef/Thy/ROOT.ML
--- a/doc-src/IsarRef/Thy/ROOT.ML	Mon Feb 09 20:37:10 2009 +0100
+++ b/doc-src/IsarRef/Thy/ROOT.ML	Mon Feb 09 21:08:59 2009 +0100
@@ -1,4 +1,4 @@
-
+set quick_and_dirty;
 set ThyOutput.source;
 use "../../antiquote_setup.ML";