equal
deleted
inserted
replaced
78 val parent_path: theory -> theory |
78 val parent_path: theory -> theory |
79 val root_path: theory -> theory |
79 val root_path: theory -> theory |
80 val add_space: string * string list -> theory -> theory |
80 val add_space: string * string list -> theory -> theory |
81 val add_name: string -> theory -> theory |
81 val add_name: string -> theory -> theory |
82 val copy: theory -> theory |
82 val copy: theory -> theory |
|
83 val prep_ext: theory -> theory |
83 val prep_ext_merge: theory list -> theory |
84 val prep_ext_merge: theory list -> theory |
84 val merge_theories: string -> theory * theory -> theory |
85 val merge_theories: string -> theory * theory -> theory |
85 val requires: theory -> string -> string -> unit |
86 val requires: theory -> string -> string -> unit |
86 val assert_super: theory -> theory -> theory |
87 val assert_super: theory -> theory -> theory |
87 val pre_pure: theory |
88 val pre_pure: theory |
209 val parent_path = add_path ".."; |
210 val parent_path = add_path ".."; |
210 val root_path = add_path "/"; |
211 val root_path = add_path "/"; |
211 val add_space = ext_sign Sign.add_space; |
212 val add_space = ext_sign Sign.add_space; |
212 val add_name = ext_sign Sign.add_name; |
213 val add_name = ext_sign Sign.add_name; |
213 val copy = ext_sign (K Sign.copy) (); |
214 val copy = ext_sign (K Sign.copy) (); |
|
215 val prep_ext = ext_sign (K Sign.prep_ext) (); |
214 |
216 |
215 |
217 |
216 |
218 |
217 (** add axioms **) |
219 (** add axioms **) |
218 |
220 |
235 (name, no_vars t) |
237 (name, no_vars t) |
236 end |
238 end |
237 handle ERROR => err_in_axm name; |
239 handle ERROR => err_in_axm name; |
238 |
240 |
239 (*some duplication of code with read_def_cterm*) |
241 (*some duplication of code with read_def_cterm*) |
240 fun read_def_axm (sg, types, sorts) used (name, str) = |
242 fun read_def_axm (sg, types, sorts) used (name, str) = |
241 let |
243 let |
242 val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str; |
244 val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str; |
243 val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); |
245 val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); |
244 in cert_axm sg (name,t) end |
246 in cert_axm sg (name,t) end |
245 handle ERROR => err_in_axm name; |
247 handle ERROR => err_in_axm name; |
408 fun get_data kind f = Sign.get_data kind f o sign_of; |
410 fun get_data kind f = Sign.get_data kind f o sign_of; |
409 fun put_data kind f = ext_sign (Sign.put_data kind f); |
411 fun put_data kind f = ext_sign (Sign.put_data kind f); |
410 |
412 |
411 |
413 |
412 |
414 |
413 (** merge theories **) (*exception ERROR*) |
415 (** merge theories **) (*exception ERROR*) |
414 |
416 |
415 fun merge_sign (sg, thy) = |
417 fun merge_sign (sg, thy) = |
416 Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg; |
418 Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg; |
417 |
419 |
418 (*merge list of theories from left to right, preparing extend*) |
420 (*merge list of theories from left to right, preparing extend*) |