24 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
24 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
25 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
25 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
26 val affirm: local_theory -> local_theory |
26 val affirm: local_theory -> local_theory |
27 val pretty: local_theory -> Pretty.T list |
27 val pretty: local_theory -> Pretty.T list |
28 val axioms: string -> |
28 val axioms: string -> |
29 ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory |
29 ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory |
30 -> (term list * (string * thm list) list) * local_theory |
30 -> (term list * (string * thm list) list) * local_theory |
31 val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> |
31 val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> |
32 (term * term) * local_theory |
32 (term * term) * local_theory |
33 val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory -> |
33 val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
34 (term * (string * thm)) * local_theory |
34 (term * (string * thm)) * local_theory |
35 val note: string -> (Name.binding * Attrib.src list) * thm list -> |
35 val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory |
36 local_theory -> (string * thm list) * local_theory |
36 val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
37 val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
|
38 local_theory -> (string * thm list) list * local_theory |
37 local_theory -> (string * thm list) list * local_theory |
39 val type_syntax: declaration -> local_theory -> local_theory |
38 val type_syntax: declaration -> local_theory -> local_theory |
40 val term_syntax: declaration -> local_theory -> local_theory |
39 val term_syntax: declaration -> local_theory -> local_theory |
41 val declaration: declaration -> local_theory -> local_theory |
40 val declaration: declaration -> local_theory -> local_theory |
42 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
41 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
55 (* type lthy *) |
54 (* type lthy *) |
56 |
55 |
57 type operations = |
56 type operations = |
58 {pretty: local_theory -> Pretty.T list, |
57 {pretty: local_theory -> Pretty.T list, |
59 axioms: string -> |
58 axioms: string -> |
60 ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory |
59 ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory -> |
61 -> (term list * (string * thm list) list) * local_theory, |
60 (term list * (string * thm list) list) * local_theory, |
62 abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory, |
61 abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> |
|
62 (term * term) * local_theory, |
63 define: string -> |
63 define: string -> |
64 (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory -> |
64 (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
65 (term * (string * thm)) * local_theory, |
65 (term * (string * thm)) * local_theory, |
66 notes: string -> |
66 notes: string -> |
67 ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
67 (Attrib.binding * (thm list * Attrib.src list) list) list -> |
68 local_theory -> (string * thm list) list * local_theory, |
68 local_theory -> (string * thm list) list * local_theory, |
69 type_syntax: declaration -> local_theory -> local_theory, |
69 type_syntax: declaration -> local_theory -> local_theory, |
70 term_syntax: declaration -> local_theory -> local_theory, |
70 term_syntax: declaration -> local_theory -> local_theory, |
71 declaration: declaration -> local_theory -> local_theory, |
71 declaration: declaration -> local_theory -> local_theory, |
72 reinit: local_theory -> local_theory, |
72 reinit: local_theory -> local_theory, |