diff -r 6fae74ee591a -r bc874d2ee55a doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Wed Jan 25 14:13:59 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Wed Jan 25 15:39:08 2012 +0100
@@ -1084,23 +1084,50 @@
 
 text %mlref {*
   \begin{mldecls}
+  @{index_ML "op RSN": "thm * (int * thm) -> thm"} \\
   @{index_ML "op RS": "thm * thm -> thm"} \\
+
+  @{index_ML "op RLN": "thm list * (int * thm list) -> thm list"} \\
+  @{index_ML "op RL": "thm list * thm list -> thm list"} \\
+
+  @{index_ML "op MRS": "thm list * thm -> thm"} \\
   @{index_ML "op OF": "thm * thm list -> thm"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text "rule\<^sub>1"} with @{text
-  "rule\<^sub>2"} according to the @{inference resolution} principle
-  explained above.  Note that the corresponding rule attribute in the
-  Isar language is called @{attribute THEN}.
+  \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of
+  @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},
+  according to the @{inference resolution} principle explained above.
+  Unless there is precisely one resolvent it raises exception @{ML
+  THM}.
+
+  This corresponds to the rule attribute @{attribute THEN} in Isar
+  source language.
+
+  \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1,
+  rule\<^sub>2)"}.
 
-  \item @{text "rule OF rules"} resolves a list of rules with the
-  first rule, addressing its premises @{text "1, \<dots>, length rules"}
-  (operating from last to first).  This means the newly emerging
-  premises are all concatenated, without interfering.  Also note that
-  compared to @{text "RS"}, the rule argument order is swapped: @{text
-  "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}.
+  \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules.  For
+  every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in
+  @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with
+  the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple
+  results in one big list.  Note that such strict enumerations of
+  higher-order unifications can be inefficient compared to the lazy
+  variant seen in elementary tactics like @{ML resolve_tac}.
+
+  \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,
+  rules\<^sub>2)"}.
+
+  \item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^isub>i"}
+  against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>,
+  1"}.  By working from right to left, newly emerging premises are
+  concatenated in the result, without interfering.
+
+  \item @{text "rule OF rules"} abbreviates @{text "rules MRS rule"}.
+
+  This corresponds to the rule attribute @{attribute OF} in Isar
+  source language.
 
   \end{description}
 *}