# HG changeset patch
# User wenzelm
# Date 1236812523 -3600
# Node ID 0b857a58b15ef45a64091cfa1b76d3bd5333471e
# Parent  00323c45ea83b00d027ae62d3293d7428e05d05e
tuned;

diff -r 00323c45ea83 -r 0b857a58b15e doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Wed Mar 11 23:59:34 2009 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Mar 12 00:02:03 2009 +0100
@@ -142,9 +142,8 @@
   compose rules by resolution.  @{attribute THEN} resolves with the
   first premise of @{text a} (an alternative position may be also
   specified); the @{attribute COMP} version skips the automatic
-  lifting process that is normally intended (cf.\ @{ML [source=false]
-  "op RS"} and @{ML [source=false] "op COMP"} in
-  \cite{isabelle-implementation}).
+  lifting process that is normally intended (cf.\ @{ML "op RS"} and
+  @{ML "op COMP"} in \cite{isabelle-implementation}).
   
   \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
   folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
diff -r 00323c45ea83 -r 0b857a58b15e doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Wed Mar 11 23:59:34 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Mar 12 00:02:03 2009 +0100
@@ -769,11 +769,11 @@
   \item @{attribute rule}~@{text del} undeclares introduction,
   elimination, or destruct rules.
   
-  \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
-  of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (in parallel).  This
-  corresponds to the @{ML [source=false] "op MRS"} operation in ML,
-  but note the reversed order.  Positions may be effectively skipped
-  by including ``@{text _}'' (underscore) as argument.
+  \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
+  theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
+  (in parallel).  This corresponds to the @{ML "op MRS"} operation in
+  ML, but note the reversed order.  Positions may be effectively
+  skipped by including ``@{text _}'' (underscore) as argument.
   
   \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
   instantiation of term variables.  The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
@@ -886,11 +886,11 @@
 
   \item @{command "method_setup"}~@{text "name = text description"}
   defines a proof method in the current theory.  The given @{text
-  "text"} has to be an ML expression of type @{ML_type [source=false]
-  "Args.src -> Proof.context -> Proof.method"}.  Parsing concrete
-  method syntax from @{ML_type Args.src} input can be quite tedious in
-  general.  The following simple examples are for methods without any
-  explicit arguments, or a list of theorems, respectively.
+  "text"} has to be an ML expression of type @{ML_type "Args.src ->
+  Proof.context -> Proof.method"}.  Parsing concrete method syntax
+  from @{ML_type Args.src} input can be quite tedious in general.  The
+  following simple examples are for methods without any explicit
+  arguments, or a list of theorems, respectively.
 
 %FIXME proper antiquotations
 {\footnotesize