| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2114 | 3201a8c3456b |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
33 thm exp_pat.induct |
33 thm exp_pat.induct |
34 thm exp_pat.distinct |
34 thm exp_pat.distinct |
35 thm exp_pat.fv |
35 thm exp_pat.fv |
36 thm exp_pat.supp(1-2) |
36 thm exp_pat.supp(1-2) |
37 |
37 |
38 declare permute_exp_raw_permute_pat_raw.simps[eqvt] |
|
39 |
|
40 equivariance alpha_exp_raw |
38 equivariance alpha_exp_raw |
41 |
39 |
42 |
40 |
43 end |
41 end |
44 |
42 |