--- 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.
--- 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";
--- 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";
--- 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";