equal
deleted
inserted
replaced
293 @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> |
293 @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> |
294 ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ |
294 ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ |
295 @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list -> |
295 @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list -> |
296 ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ |
296 ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ |
297 @{index_ML Obtain.result: "(Proof.context -> tactic) -> |
297 @{index_ML Obtain.result: "(Proof.context -> tactic) -> |
298 thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} |
298 thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\ |
299 \end{mldecls} |
299 \end{mldecls} |
300 |
300 |
301 \begin{description} |
301 \begin{description} |
302 |
302 |
303 \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a |
303 \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a |