--- a/src/Doc/IsarImplementation/Tactic.thy Thu Jun 27 11:07:48 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy Thu Jun 27 11:33:42 2013 +0200
@@ -491,7 +491,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
- @{index_ML compose: "thm * int * thm -> thm list"} \\
+ @{index_ML Drule.compose: "thm * int * thm -> thm list"} \\
@{index_ML_op COMP: "thm * thm -> thm"} \\
\end{mldecls}
@@ -505,14 +505,14 @@
performs elim-resolution --- it solves the first premise of @{text
"rule"} by assumption and deletes that assumption.
- \item @{ML compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
+ \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
regarded as an atomic formula, to solve premise @{text "i"} of
@{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
"\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. For each @{text "s"} that unifies
@{text "\<psi>"} and @{text "\<phi>"}, the result list contains the theorem
@{text "(\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.
- \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "compose (thm\<^sub>1, 1,
+ \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "Drule.compose (thm\<^sub>1, 1,
thm\<^sub>2)"} and returns the result, if unique; otherwise, it raises
exception @{ML THM}.
--- a/src/Pure/drule.ML Thu Jun 27 11:07:48 2013 +0200
+++ b/src/Pure/drule.ML Thu Jun 27 11:33:42 2013 +0200
@@ -34,7 +34,6 @@
val RL: thm list * thm list -> thm list
val MRS: thm list * thm -> thm
val OF: thm * thm list -> thm
- val compose: thm * int * thm -> thm list
val COMP: thm * thm -> thm
val INCR_COMP: thm * thm -> thm
val COMP_INCR: thm * thm -> thm
@@ -69,6 +68,7 @@
val store_standard_thm_open: binding -> thm -> thm
val multi_resolve: thm list -> thm -> thm Seq.seq
val multi_resolves: thm list -> thm list -> thm Seq.seq
+ val compose: thm * int * thm -> thm list
val compose_single: thm * int * thm -> thm
val equals_cong: thm
val imp_cong: thm