equal
deleted
inserted
replaced
4 Overloaded definitions without any discipline. |
4 Overloaded definitions without any discipline. |
5 *) |
5 *) |
6 |
6 |
7 signature OVERLOADING = |
7 signature OVERLOADING = |
8 sig |
8 sig |
9 val init: (string * (string * typ) * bool) list -> theory -> local_theory |
9 val init: (string * (string * typ) * bool) list -> theory -> Proof.context |
10 val conclude: local_theory -> local_theory |
10 val conclude: local_theory -> local_theory |
11 val declare: string * typ -> theory -> term * theory |
11 val declare: string * typ -> theory -> term * theory |
12 val confirm: binding -> local_theory -> local_theory |
12 val confirm: binding -> local_theory -> local_theory |
13 val define: bool -> binding -> string * term -> theory -> thm * theory |
13 val define: bool -> binding -> string * term -> theory -> thm * theory |
14 val operation: Proof.context -> binding -> (string * bool) option |
14 val operation: Proof.context -> binding -> (string * bool) option |