set quick_and_dirty;
authorwenzelm
Mon, 09 Feb 2009 21:08:59 +0100
changeset 29720 020861892625
parent 29719 d2597c4f7e5c
child 29721 df4e53d18ebc
set quick_and_dirty;
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";