111 \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\ |
111 \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\ |
112 \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
112 \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
113 \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
113 \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
114 \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% |
114 \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% |
115 \verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\ |
115 \verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\ |
116 \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\ |
116 \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\ |
117 \end{mldecls} |
117 \end{mldecls} |
118 |
118 |
119 \begin{description} |
119 \begin{description} |
120 |
120 |
121 \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |
121 \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |
322 % |
322 % |
323 \isatagmlref |
323 \isatagmlref |
324 % |
324 % |
325 \begin{isamarkuptext}% |
325 \begin{isamarkuptext}% |
326 \begin{mldecls} |
326 \begin{mldecls} |
327 \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline% |
327 \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\ |
328 \verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline% |
|
329 \verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\ |
|
330 \end{mldecls} |
328 \end{mldecls} |
331 \begin{mldecls} |
329 \begin{mldecls} |
332 \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
330 \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
333 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
331 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
334 \indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
332 \indexdef{}{ML}{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| \\ |
333 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
336 \end{mldecls} |
334 \end{mldecls} |
337 \begin{mldecls} |
335 \begin{mldecls} |
338 \indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline% |
336 \indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline% |
339 \verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\ |
337 \verb| thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\ |
340 \end{mldecls} |
338 \end{mldecls} |
341 |
339 |
342 \begin{description} |
340 \begin{description} |
343 |
341 |
344 \item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure |
342 \item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure |