equal
deleted
inserted
replaced
231 fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy; |
231 fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy; |
232 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; |
232 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; |
233 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; |
233 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; |
234 |
234 |
235 val intern_class = Name_Space.intern o class_space; |
235 val intern_class = Name_Space.intern o class_space; |
236 val extern_class = Name_Space.extern o class_space; |
236 fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy); |
237 val intern_type = Name_Space.intern o type_space; |
237 val intern_type = Name_Space.intern o type_space; |
238 val extern_type = Name_Space.extern o type_space; |
238 fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy); |
239 val intern_const = Name_Space.intern o const_space; |
239 val intern_const = Name_Space.intern o const_space; |
240 val extern_const = Name_Space.extern o const_space; |
240 fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy); |
241 |
241 |
242 |
242 |
243 |
243 |
244 (** certify entities **) (*exception TYPE*) |
244 (** certify entities **) (*exception TYPE*) |
245 |
245 |