equal
deleted
inserted
replaced
332 \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
332 \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
333 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
333 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
334 \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
334 \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
335 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
335 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
336 \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline% |
336 \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline% |
337 \verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| |
337 \verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\ |
338 \end{mldecls} |
338 \end{mldecls} |
339 |
339 |
340 \begin{description} |
340 \begin{description} |
341 |
341 |
342 \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a |
342 \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a |