25 ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory |
25 ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory |
26 val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
26 val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
27 (bstring * thm list) list * local_theory |
27 (bstring * thm list) list * local_theory |
28 val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> |
28 val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> |
29 (term * term) * local_theory |
29 (term * term) * local_theory |
30 val defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> |
30 val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
31 local_theory -> (term * (bstring * thm)) list * local_theory |
31 local_theory -> (term * (bstring * thm)) * local_theory |
32 val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
32 val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
33 local_theory -> (bstring * thm list) list * local_theory |
33 local_theory -> (bstring * thm list) list * local_theory |
34 val type_syntax: declaration -> local_theory -> local_theory |
34 val type_syntax: declaration -> local_theory -> local_theory |
35 val term_syntax: declaration -> local_theory -> local_theory |
35 val term_syntax: declaration -> local_theory -> local_theory |
36 val declaration: declaration -> local_theory -> local_theory |
36 val declaration: declaration -> local_theory -> local_theory |
37 val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
|
38 local_theory -> (term * (bstring * thm)) * local_theory |
|
39 val note: string -> (bstring * Attrib.src list) * thm list -> |
37 val note: string -> (bstring * Attrib.src list) * thm list -> |
40 local_theory -> (bstring * thm list) * local_theory |
38 local_theory -> (bstring * thm list) * local_theory |
41 val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
39 val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
42 val target_morphism: local_theory -> morphism |
40 val target_morphism: local_theory -> morphism |
43 val target_naming: local_theory -> NameSpace.naming |
41 val target_naming: local_theory -> NameSpace.naming |
60 consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory -> |
58 consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory -> |
61 (term * thm) list * local_theory, |
59 (term * thm) list * local_theory, |
62 axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
60 axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
63 (bstring * thm list) list * local_theory, |
61 (bstring * thm list) list * local_theory, |
64 abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory, |
62 abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory, |
65 defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> |
63 def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
66 local_theory -> (term * (bstring * thm)) list * local_theory, |
64 local_theory -> (term * (bstring * thm)) * local_theory, |
67 notes: string -> |
65 notes: string -> |
68 ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
66 ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
69 local_theory -> (bstring * thm list) list * local_theory, |
67 local_theory -> (bstring * thm list) list * local_theory, |
70 type_syntax: declaration -> local_theory -> local_theory, |
68 type_syntax: declaration -> local_theory -> local_theory, |
71 term_syntax: declaration -> local_theory -> local_theory, |
69 term_syntax: declaration -> local_theory -> local_theory, |
72 declaration: declaration -> local_theory -> local_theory, |
70 declaration: declaration -> local_theory -> local_theory, |
73 target_morphism: local_theory -> morphism, |
|
74 target_naming: local_theory -> NameSpace.naming, |
71 target_naming: local_theory -> NameSpace.naming, |
75 reinit: local_theory -> theory -> local_theory, |
72 reinit: local_theory -> theory -> local_theory, |
76 exit: local_theory -> Proof.context}; |
73 exit: local_theory -> Proof.context}; |
77 |
74 |
78 datatype lthy = LThy of |
75 datatype lthy = LThy of |
155 |
152 |
156 val pretty = operation #pretty; |
153 val pretty = operation #pretty; |
157 val consts = operation2 #consts; |
154 val consts = operation2 #consts; |
158 val axioms = operation2 #axioms; |
155 val axioms = operation2 #axioms; |
159 val abbrev = operation2 #abbrev; |
156 val abbrev = operation2 #abbrev; |
160 val defs = operation2 #defs; |
157 val def = operation2 #def; |
161 val notes = operation2 #notes; |
158 val notes = operation2 #notes; |
162 val type_syntax = operation1 #type_syntax; |
159 val type_syntax = operation1 #type_syntax; |
163 val term_syntax = operation1 #term_syntax; |
160 val term_syntax = operation1 #term_syntax; |
164 val declaration = operation1 #declaration; |
161 val declaration = operation1 #declaration; |
165 val target_morphism = operation #target_morphism; |
|
166 val target_naming = operation #target_naming; |
162 val target_naming = operation #target_naming; |
167 |
163 |
168 fun def kind arg lthy = lthy |> defs kind [arg] |>> hd; |
|
169 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd; |
164 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd; |
|
165 |
|
166 fun target_morphism lthy = |
|
167 ProofContext.export_morphism lthy (target_of lthy) $> |
|
168 Morphism.thm_morphism Goal.norm_result; |
170 |
169 |
171 fun notation mode raw_args lthy = |
170 fun notation mode raw_args lthy = |
172 let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args |
171 let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args |
173 in term_syntax (ProofContext.target_notation mode args) lthy end; |
172 in term_syntax (ProofContext.target_notation mode args) lthy end; |
174 |
173 |