search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

Rename syl6eq to eqtrdi #4074

Closed jkingdon closed 1 week ago

jkingdon commented 2 weeks ago

This is in set.mm and iset.mm

tirix commented 1 week ago

That's much better!

wlammen commented 1 week ago

I checked all lines by shortly glancing at it, to see whether something unexpected was pushed.

This pull request could have been split in two halves, by moving syl6eqr unchanged to the end of main, and then perform the replacement in the first half first, and proceed with the rest in a second PR.

jkingdon commented 1 week ago

Thanks to all the reviewers.

As for splitting it, I guess maybe I will if there is another one this big. I haven't checked the size of the remaining proposed changes but I suppose some of them are probably also large.