1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Wed Mar 11 23:59:34 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Mar 12 00:02:03 2009 +0100
     1.3 @@ -769,11 +769,11 @@
     1.4    \item @{attribute rule}~@{text del} undeclares introduction,
     1.5    elimination, or destruct rules.
     1.6    
     1.7 -  \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
     1.8 -  of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (in parallel).  This
     1.9 -  corresponds to the @{ML [source=false] "op MRS"} operation in ML,
    1.10 -  but note the reversed order.  Positions may be effectively skipped
    1.11 -  by including ``@{text _}'' (underscore) as argument.
    1.12 +  \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
    1.13 +  theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
    1.14 +  (in parallel).  This corresponds to the @{ML "op MRS"} operation in
    1.15 +  ML, but note the reversed order.  Positions may be effectively
    1.16 +  skipped by including ``@{text _}'' (underscore) as argument.
    1.17    
    1.18    \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
    1.19    instantiation of term variables.  The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
    1.20 @@ -886,11 +886,11 @@
    1.21  
    1.22    \item @{command "method_setup"}~@{text "name = text description"}
    1.23    defines a proof method in the current theory.  The given @{text
    1.24 -  "text"} has to be an ML expression of type @{ML_type [source=false]
    1.25 -  "Args.src -> Proof.context -> Proof.method"}.  Parsing concrete
    1.26 -  method syntax from @{ML_type Args.src} input can be quite tedious in
    1.27 -  general.  The following simple examples are for methods without any
    1.28 -  explicit arguments, or a list of theorems, respectively.
    1.29 +  "text"} has to be an ML expression of type @{ML_type "Args.src ->
    1.30 +  Proof.context -> Proof.method"}.  Parsing concrete method syntax
    1.31 +  from @{ML_type Args.src} input can be quite tedious in general.  The
    1.32 +  following simple examples are for methods without any explicit
    1.33 +  arguments, or a list of theorems, respectively.
    1.34  
    1.35  %FIXME proper antiquotations
    1.36  {\footnotesize