doc-src/IsarRef/Thy/ML_Tactic.thy

   \item The ``mode'' of resolution: intro, elim, destruct, or forward
   (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
   @{ML forward_tac}).
 
   \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
-  @{ML res_inst_tac}).
+  @{ML RuleInsts.res_inst_tac}).
 
   \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
   vs.\ @{ML rtac}).
 
   \end{enumerate}

 
   \medskip
   \begin{tabular}{lll}
     @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
     @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
-    @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
+    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
     @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
     @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
     @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
-    @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
+    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
     @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
   \end{tabular}
   \medskip
 
   Note that explicit goal addressing may be usually avoided by