# HG changeset patch
# User wenzelm
# Date 1210158346 -7200
# Node ID 46b6306c181ee99c24bf0767e019185c87521c04
# Parent  612ca951afee318bb7abef3ff072c5320dd7cebd
enabled ThyOutput.source option by default;

diff -r 612ca951afee -r 46b6306c181e doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Wed May 07 13:05:13 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Wed May 07 13:05:46 2008 +0200
@@ -1090,8 +1090,8 @@
   theorem by @{text n} (default 1).
 
   \item [@{attribute Pure.elim_format}] turns a destruction rule into
-  elimination rule format, by resolving with the rule @{prop [source]
-  "PROP A \<Longrightarrow> (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
+  elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
+  (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   
   Note that the Classical Reasoner (\secref{sec:classical}) provides
   its own version of this operation.
diff -r 612ca951afee -r 46b6306c181e doc-src/IsarRef/Thy/ROOT-HOLCF.ML
--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed May 07 13:05:13 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed May 07 13:05:46 2008 +0200
@@ -1,5 +1,7 @@
 
 (* $Id$ *)
 
+set ThyOutput.source;
 use "../../antiquote_setup.ML";
+
 use_thy "HOLCF_Specific";
diff -r 612ca951afee -r 46b6306c181e doc-src/IsarRef/Thy/ROOT-ZF.ML
--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed May 07 13:05:13 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed May 07 13:05:46 2008 +0200
@@ -1,5 +1,7 @@
 
 (* $Id$ *)
 
+set ThyOutput.source;
 use "../../antiquote_setup.ML";
+
 use_thy "ZF_Specific";
diff -r 612ca951afee -r 46b6306c181e doc-src/IsarRef/Thy/ROOT.ML
--- a/doc-src/IsarRef/Thy/ROOT.ML	Wed May 07 13:05:13 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML	Wed May 07 13:05:46 2008 +0200
@@ -1,7 +1,9 @@
 
 (* $Id$ *)
 
+set ThyOutput.source;
 use "../../antiquote_setup.ML";
+
 use_thy "intro";
 use_thy "syntax";
 use_thy "pure";