22 val smart_theorems: string -> xstring option -> |
22 val smart_theorems: string -> xstring option -> |
23 ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list -> |
23 ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list -> |
24 theory -> Proof.context * theory |
24 theory -> Proof.context * theory |
25 val declare_theorems: xstring option -> |
25 val declare_theorems: xstring option -> |
26 (thmref * Attrib.src list) list -> theory -> Proof.context * theory |
26 (thmref * Attrib.src list) list -> theory -> Proof.context * theory |
27 val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
27 val have: ((string * Attrib.src list) * (string * string list) list) list -> |
28 bool -> Proof.state -> Proof.state |
28 bool -> Proof.state -> Proof.state |
29 val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
29 val hence: ((string * Attrib.src list) * (string * string list) list) list -> |
30 bool -> Proof.state -> Proof.state |
30 bool -> Proof.state -> Proof.state |
31 val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
31 val show: ((string * Attrib.src list) * (string * string list) list) list -> |
32 bool -> Proof.state -> Proof.state |
32 bool -> Proof.state -> Proof.state |
33 val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
33 val thus: ((string * Attrib.src list) * (string * string list) list) list -> |
34 bool -> Proof.state -> Proof.state |
34 bool -> Proof.state -> Proof.state |
35 val theorem: string -> string * Attrib.src list -> string * (string list * string list) -> |
35 val theorem: string -> string * Attrib.src list -> string * string list -> theory -> Proof.state |
36 theory -> Proof.state |
36 val theorem_i: string -> string * attribute list -> term * term list -> theory -> Proof.state |
37 val theorem_i: string -> string * attribute list -> term * (term list * term list) -> |
|
38 theory -> Proof.state |
|
39 val qed: Method.text option -> Toplevel.transition -> Toplevel.transition |
37 val qed: Method.text option -> Toplevel.transition -> Toplevel.transition |
40 val terminal_proof: Method.text * Method.text option -> |
38 val terminal_proof: Method.text * Method.text option -> |
41 Toplevel.transition -> Toplevel.transition |
39 Toplevel.transition -> Toplevel.transition |
42 val default_proof: Toplevel.transition -> Toplevel.transition |
40 val default_proof: Toplevel.transition -> Toplevel.transition |
43 val immediate_proof: Toplevel.transition -> Toplevel.transition |
41 val immediate_proof: Toplevel.transition -> Toplevel.transition |