equal
deleted
inserted
replaced
89 |
89 |
90 (* Tactics *) |
90 (* Tactics *) |
91 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic |
91 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic |
92 |
92 |
93 (* Storing results *) |
93 (* Storing results *) |
|
94 val local_note_prefix: string -> |
|
95 (Name.binding * attribute list) * (thm list * attribute list) list -> |
|
96 Proof.context -> (string * thm list) * Proof.context |
94 val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
97 val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
95 Proof.context -> Proof.context |
98 Proof.context -> Proof.context |
96 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context |
99 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context |
97 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context |
100 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context |
98 val add_declaration: string -> declaration -> Proof.context -> Proof.context |
101 val add_declaration: string -> declaration -> Proof.context -> Proof.context |