Please help us finish removing Part 18 (Additional material, deprecated)

[David A. Wheeler]

Many of the theorems in Part 18 (Additional material, deprecated) now have an extensible structure version. Indeed, it looks to me like it's mostly moved. So the current plan is to remove that part in the very near future.

If there is anything in there that needs saving, but has not been saved/transitioned yet, please help us do that. (The discussion about magmas etc. is only a small part of this discussion.)

Discussion about removing this deprecated part is here:
https://github.com/metamath/set.mm/issues/1432

Also, an additional note. If you converted some existing theorem that did not use extensible structures over to the extensible structure version, please make sure you include the original contributor and the original date in it. That is the right thing to do, of course. Also, I intend to recreate the Gourse visualization later this year, and once the old theorems go away it will depend on the presence of those date and contributor names so that the original contributors will be credited. Of course, if you develop the theorem independently instead of working off the older version, then giving credit to an unrelated theorem would not be the right thing to do.


--- David A.Wheeler