19 val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory |
19 val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory |
20 val declaration: string * Position.T -> local_theory -> local_theory |
20 val declaration: string * Position.T -> local_theory -> local_theory |
21 val simproc_setup: string -> string list -> string * Position.T -> string list -> |
21 val simproc_setup: string -> string list -> string * Position.T -> string list -> |
22 local_theory -> local_theory |
22 local_theory -> local_theory |
23 val hide_names: bool -> string * xstring list -> theory -> theory |
23 val hide_names: bool -> string * xstring list -> theory -> theory |
24 val have: ((Name.binding * Attrib.src list) * (string * string list) list) list -> |
24 val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
25 bool -> Proof.state -> Proof.state |
25 val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
26 val hence: ((Name.binding * Attrib.src list) * (string * string list) list) list -> |
26 val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
27 bool -> Proof.state -> Proof.state |
27 val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
28 val show: ((Name.binding * Attrib.src list) * (string * string list) list) list -> |
|
29 bool -> Proof.state -> Proof.state |
|
30 val thus: ((Name.binding * Attrib.src list) * (string * string list) list) list -> |
|
31 bool -> Proof.state -> Proof.state |
|
32 val qed: Method.text option -> Toplevel.transition -> Toplevel.transition |
28 val qed: Method.text option -> Toplevel.transition -> Toplevel.transition |
33 val terminal_proof: Method.text * Method.text option -> |
29 val terminal_proof: Method.text * Method.text option -> |
34 Toplevel.transition -> Toplevel.transition |
30 Toplevel.transition -> Toplevel.transition |
35 val default_proof: Toplevel.transition -> Toplevel.transition |
31 val default_proof: Toplevel.transition -> Toplevel.transition |
36 val immediate_proof: Toplevel.transition -> Toplevel.transition |
32 val immediate_proof: Toplevel.transition -> Toplevel.transition |