41 local_theory -> local_theory |
41 local_theory -> local_theory |
42 val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string -> |
42 val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string -> |
43 local_theory -> local_theory |
43 local_theory -> local_theory |
44 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
44 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
45 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
45 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
46 val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list |
46 val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
47 -> local_theory -> (bstring * thm list) list * local_theory |
47 local_theory -> (bstring * thm list) list * local_theory |
48 val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
48 val theorems_cmd: string -> |
49 -> local_theory -> (bstring * thm list) list * local_theory |
49 ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list -> |
|
50 local_theory -> (bstring * thm list) list * local_theory |
50 val theorem: string -> Method.text option -> |
51 val theorem: string -> Method.text option -> |
51 (thm list list -> local_theory -> local_theory) -> |
52 (thm list list -> local_theory -> local_theory) -> |
52 string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i -> |
53 string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i -> |
53 bool -> local_theory -> Proof.state |
54 bool -> local_theory -> Proof.state |
54 val theorem_cmd: string -> Method.text option -> |
55 val theorem_cmd: string -> Method.text option -> |