| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2120 | 2786ff1df475 |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
30 thm exp_pat.perm |
30 thm exp_pat.perm |
31 thm exp_pat.induct |
31 thm exp_pat.induct |
32 thm exp_pat.distinct |
32 thm exp_pat.distinct |
33 thm exp_pat.supp |
33 thm exp_pat.supp |
34 |
34 |
35 declare permute_exp_raw_permute_pat_raw.simps[eqvt] |
|
36 |
|
37 equivariance alpha_exp_raw |
35 equivariance alpha_exp_raw |
38 |
36 |
39 |
37 |
40 end |
38 end |
41 |
39 |