equal
deleted
inserted
replaced
45 val const_instance: theory -> string * typ list -> typ |
45 val const_instance: theory -> string * typ list -> typ |
46 val mk_const: theory -> string * typ list -> term |
46 val mk_const: theory -> string * typ list -> term |
47 val class_space: theory -> Name_Space.T |
47 val class_space: theory -> Name_Space.T |
48 val type_space: theory -> Name_Space.T |
48 val type_space: theory -> Name_Space.T |
49 val const_space: theory -> Name_Space.T |
49 val const_space: theory -> Name_Space.T |
|
50 val class_alias: binding -> class -> theory -> theory |
|
51 val type_alias: binding -> string -> theory -> theory |
|
52 val const_alias: binding -> string -> theory -> theory |
50 val intern_class: theory -> xstring -> string |
53 val intern_class: theory -> xstring -> string |
51 val extern_class: theory -> string -> xstring |
54 val extern_class: theory -> string -> xstring |
52 val intern_type: theory -> xstring -> string |
55 val intern_type: theory -> xstring -> string |
53 val extern_type: theory -> string -> xstring |
56 val extern_type: theory -> string -> xstring |
54 val intern_const: theory -> xstring -> string |
57 val intern_const: theory -> xstring -> string |
231 |
234 |
232 val class_space = Type.class_space o tsig_of; |
235 val class_space = Type.class_space o tsig_of; |
233 val type_space = Type.type_space o tsig_of; |
236 val type_space = Type.type_space o tsig_of; |
234 val const_space = Consts.space_of o consts_of; |
237 val const_space = Consts.space_of o consts_of; |
235 |
238 |
|
239 fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy; |
|
240 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; |
|
241 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; |
|
242 |
236 val intern_class = Name_Space.intern o class_space; |
243 val intern_class = Name_Space.intern o class_space; |
237 val extern_class = Name_Space.extern o class_space; |
244 val extern_class = Name_Space.extern o class_space; |
238 val intern_type = Name_Space.intern o type_space; |
245 val intern_type = Name_Space.intern o type_space; |
239 val extern_type = Name_Space.extern o type_space; |
246 val extern_type = Name_Space.extern o type_space; |
240 val intern_const = Name_Space.intern o const_space; |
247 val intern_const = Name_Space.intern o const_space; |