equal
deleted
inserted
replaced
139 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context |
139 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context |
140 val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> |
140 val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> |
141 Context.generic -> Context.generic |
141 Context.generic -> Context.generic |
142 val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> |
142 val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> |
143 Context.generic -> Context.generic |
143 Context.generic -> Context.generic |
|
144 val target_naming_of: Context.generic -> Name_Space.naming |
144 val class_alias: binding -> class -> Proof.context -> Proof.context |
145 val class_alias: binding -> class -> Proof.context -> Proof.context |
145 val type_alias: binding -> string -> Proof.context -> Proof.context |
146 val type_alias: binding -> string -> Proof.context -> Proof.context |
146 val const_alias: binding -> string -> Proof.context -> Proof.context |
147 val const_alias: binding -> string -> Proof.context -> Proof.context |
147 val add_const_constraint: string * typ option -> Proof.context -> Proof.context |
148 val add_const_constraint: string * typ option -> Proof.context -> Proof.context |
148 val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context |
149 val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context |
990 in Context.mapping (Sign.notation add mode args') (notation add mode args') end; |
991 in Context.mapping (Sign.notation add mode args') (notation add mode args') end; |
991 |
992 |
992 end; |
993 end; |
993 |
994 |
994 |
995 |
|
996 (* naming *) |
|
997 |
|
998 val target_naming_of = Context.cases Sign.naming_of naming_of; |
|
999 |
|
1000 |
995 (* aliases *) |
1001 (* aliases *) |
996 |
1002 |
997 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; |
1003 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; |
998 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; |
1004 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; |
999 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; |
1005 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; |