1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Wed May 07 13:05:13 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Wed May 07 13:05:46 2008 +0200
     1.3 @@ -1090,8 +1090,8 @@
     1.4    theorem by @{text n} (default 1).
     1.5  
     1.6    \item [@{attribute Pure.elim_format}] turns a destruction rule into
     1.7 -  elimination rule format, by resolving with the rule @{prop [source]
     1.8 -  "PROP A \<Longrightarrow> (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
     1.9 +  elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
    1.10 +  (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
    1.11    
    1.12    Note that the Classical Reasoner (\secref{sec:classical}) provides
    1.13    its own version of this operation.

     2.1 --- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed May 07 13:05:13 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed May 07 13:05:46 2008 +0200
     2.3 @@ -1,5 +1,7 @@
     2.4  
     2.5  (* $Id$ *)
     2.6  
     2.7 +set ThyOutput.source;
     2.8  use "../../antiquote_setup.ML";
     2.9 +
    2.10  use_thy "HOLCF_Specific";

     3.1 --- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed May 07 13:05:13 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed May 07 13:05:46 2008 +0200
     3.3 @@ -1,5 +1,7 @@
     3.4  
     3.5  (* $Id$ *)
     3.6  
     3.7 +set ThyOutput.source;
     3.8  use "../../antiquote_setup.ML";
     3.9 +
    3.10  use_thy "ZF_Specific";

     4.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Wed May 07 13:05:13 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Wed May 07 13:05:46 2008 +0200
     4.3 @@ -1,7 +1,9 @@
     4.4  
     4.5  (* $Id$ *)
     4.6  
     4.7 +set ThyOutput.source;
     4.8  use "../../antiquote_setup.ML";
     4.9 +
    4.10  use_thy "intro";
    4.11  use_thy "syntax";
    4.12  use_thy "pure";