| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2114 | 3201a8c3456b |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
66 alpha (ImpR_raw coname1 name trm_raw coname2) |
66 alpha (ImpR_raw coname1 name trm_raw coname2) |
67 (ImpR_raw coname1a namea trm_rawa coname2a)" |
67 (ImpR_raw coname1a namea trm_rawa coname2a)" |
68 |
68 |
69 thm alpha.intros |
69 thm alpha.intros |
70 |
70 |
71 declare permute_trm_raw.simps[eqvt] |
|
72 |
|
73 equivariance alpha |
71 equivariance alpha |
74 equivariance alpha_trm_raw |
72 equivariance alpha_trm_raw |
75 thm eqvts_raw |
73 thm eqvts_raw |
76 |
74 |
77 |
75 |