14 val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory |
14 val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory |
15 val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory |
15 val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory |
16 val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory |
16 val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory |
17 val add_axioms: (Attrib.binding * string) list -> theory -> theory |
17 val add_axioms: (Attrib.binding * string) list -> theory -> theory |
18 val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory |
18 val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory |
19 val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory |
19 val declaration: {syntax: bool, pervasive: bool} -> |
|
20 Symbol_Pos.text * Position.T -> local_theory -> local_theory |
20 val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list -> |
21 val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list -> |
21 local_theory -> local_theory |
22 local_theory -> local_theory |
22 val hide_class: bool -> xstring list -> theory -> theory |
23 val hide_class: bool -> xstring list -> theory -> theory |
23 val hide_type: bool -> xstring list -> theory -> theory |
24 val hide_type: bool -> xstring list -> theory -> theory |
24 val hide_const: bool -> xstring list -> theory -> theory |
25 val hide_const: bool -> xstring list -> theory -> theory |
178 |> snd; |
179 |> snd; |
179 |
180 |
180 |
181 |
181 (* declarations *) |
182 (* declarations *) |
182 |
183 |
183 fun declaration pervasive (txt, pos) = |
184 fun declaration {syntax, pervasive} (txt, pos) = |
184 ML_Lex.read pos txt |
185 ML_Lex.read pos txt |
185 |> ML_Context.expression pos |
186 |> ML_Context.expression pos |
186 "val declaration: Morphism.declaration" |
187 "val declaration: Morphism.declaration" |
187 ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)") |
188 ("Context.map_proof (Local_Theory." ^ |
|
189 (if syntax then "syntax_declaration" else "declaration") ^ " " ^ |
|
190 Bool.toString pervasive ^ " declaration)") |
188 |> Context.proof_map; |
191 |> Context.proof_map; |
189 |
192 |
190 |
193 |
191 (* simprocs *) |
194 (* simprocs *) |
192 |
195 |