equal
deleted
inserted
replaced
37 \item The ``mode'' of resolution: intro, elim, destruct, or forward |
37 \item The ``mode'' of resolution: intro, elim, destruct, or forward |
38 (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac}, |
38 (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac}, |
39 @{ML forward_tac}). |
39 @{ML forward_tac}). |
40 |
40 |
41 \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ |
41 \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ |
42 @{ML res_inst_tac}). |
42 @{ML Rule_Insts.res_inst_tac}). |
43 |
43 |
44 \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} |
44 \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} |
45 vs.\ @{ML rtac}). |
45 vs.\ @{ML rtac}). |
46 |
46 |
47 \end{enumerate} |
47 \end{enumerate} |
61 |
61 |
62 \medskip |
62 \medskip |
63 \begin{tabular}{lll} |
63 \begin{tabular}{lll} |
64 @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ |
64 @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ |
65 @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\ |
65 @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\ |
66 @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & & |
66 @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & & |
67 @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex] |
67 @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex] |
68 @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ |
68 @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ |
69 @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\ |
69 @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\ |
70 @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & & |
70 @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & & |
71 @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\ |
71 @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\ |
72 \end{tabular} |
72 \end{tabular} |
73 \medskip |
73 \medskip |
74 |
74 |
75 Note that explicit goal addressing may be usually avoided by |
75 Note that explicit goal addressing may be usually avoided by |