133 INCOMPATIBILITY. |
133 INCOMPATIBILITY. |
134 |
134 |
135 * Renamed facts about the power operation on relations, i.e., relpow |
135 * Renamed facts about the power operation on relations, i.e., relpow |
136 to match the constant's name: |
136 to match the constant's name: |
137 |
137 |
138 rel_pow_1 ~> lemma relpow_1 |
138 rel_pow_1 ~> relpow_1 |
139 rel_pow_0_I ~> relpow_0_I |
139 rel_pow_0_I ~> relpow_0_I |
140 rel_pow_Suc_I ~> relpow_Suc_I |
140 rel_pow_Suc_I ~> relpow_Suc_I |
141 rel_pow_Suc_I2 ~> relpow_Suc_I2 |
141 rel_pow_Suc_I2 ~> relpow_Suc_I2 |
142 rel_pow_0_E ~> relpow_0_E |
142 rel_pow_0_E ~> relpow_0_E |
143 rel_pow_Suc_E ~> relpow_Suc_E |
143 rel_pow_Suc_E ~> relpow_Suc_E |
144 rel_pow_E ~> relpow_E |
144 rel_pow_E ~> relpow_E |
145 rel_pow_Suc_D2 ~> lemma relpow_Suc_D2 |
145 rel_pow_Suc_D2 ~> relpow_Suc_D2 |
146 rel_pow_Suc_E2 ~> relpow_Suc_E2 |
146 rel_pow_Suc_E2 ~> relpow_Suc_E2 |
147 rel_pow_Suc_D2' ~> relpow_Suc_D2' |
147 rel_pow_Suc_D2' ~> relpow_Suc_D2' |
148 rel_pow_E2 ~> relpow_E2 |
148 rel_pow_E2 ~> relpow_E2 |
149 rel_pow_add ~> relpow_add |
149 rel_pow_add ~> relpow_add |
150 rel_pow_commute ~> relpow |
150 rel_pow_commute ~> relpow |