equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 |
8 |
9 signature NOMINAL_EQVT = |
9 signature NOMINAL_EQVT = |
10 sig |
10 sig |
11 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
|
12 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
|
13 |
|
14 val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
11 val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
15 val equivariance: string -> Proof.context -> (thm list * local_theory) |
12 val equivariance: string -> Proof.context -> (thm list * local_theory) |
16 val equivariance_cmd: string -> Proof.context -> local_theory |
13 val equivariance_cmd: string -> Proof.context -> local_theory |
17 end |
14 end |
18 |
15 |