--- a/doc-src/IsarRef/Thy/ML_Tactic.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Sat Jun 14 23:19:51 2008 +0200
@@ -41,7 +41,7 @@
@{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}).
@@ -66,11 +66,11 @@
\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