equal
deleted
inserted
replaced
51 val type_space: theory -> Name_Space.T |
51 val type_space: theory -> Name_Space.T |
52 val const_space: theory -> Name_Space.T |
52 val const_space: theory -> Name_Space.T |
53 val intern_class: theory -> xstring -> string |
53 val intern_class: theory -> xstring -> string |
54 val intern_type: theory -> xstring -> string |
54 val intern_type: theory -> xstring -> string |
55 val intern_const: theory -> xstring -> string |
55 val intern_const: theory -> xstring -> string |
56 val class_alias: binding -> class -> theory -> theory |
|
57 val type_alias: binding -> string -> theory -> theory |
56 val type_alias: binding -> string -> theory -> theory |
58 val const_alias: binding -> string -> theory -> theory |
57 val const_alias: binding -> string -> theory -> theory |
59 val arity_number: theory -> string -> int |
58 val arity_number: theory -> string -> int |
60 val arity_sorts: theory -> string -> sort -> sort list |
59 val arity_sorts: theory -> string -> sort -> sort list |
61 val certify_class: theory -> class -> class |
60 val certify_class: theory -> class -> class |
244 |
243 |
245 val intern_class = Name_Space.intern o class_space; |
244 val intern_class = Name_Space.intern o class_space; |
246 val intern_type = Name_Space.intern o type_space; |
245 val intern_type = Name_Space.intern o type_space; |
247 val intern_const = Name_Space.intern o const_space; |
246 val intern_const = Name_Space.intern o const_space; |
248 |
247 |
249 fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy; |
|
250 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; |
248 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; |
251 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; |
249 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; |
252 |
250 |
253 |
251 |
254 |
252 |