equal
deleted
inserted
replaced
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 add_const_constraint: string * typ option -> Proof.context -> Proof.context |
144 val add_const_constraint: string * typ option -> Proof.context -> Proof.context |
145 val add_abbrev: string -> Markup.property list -> |
145 val add_abbrev: string -> Markup.property list -> |
146 bstring * term -> Proof.context -> (term * term) * Proof.context |
146 bstring * term -> Proof.context -> (term * term) * Proof.context |
147 val standard_infer_types: Proof.context -> term list -> term list |
|
148 val revert_abbrev: string -> string -> Proof.context -> Proof.context |
147 val revert_abbrev: string -> string -> Proof.context -> Proof.context |
149 val verbose: bool ref |
148 val verbose: bool ref |
150 val setmp_verbose: ('a -> 'b) -> 'a -> 'b |
149 val setmp_verbose: ('a -> 'b) -> 'a -> 'b |
151 val print_syntax: Proof.context -> unit |
150 val print_syntax: Proof.context -> unit |
152 val print_abbrevs: Proof.context -> unit |
151 val print_abbrevs: Proof.context -> unit |