I just noticed that
theories/Reals has 5 files Ranalysis1 through Ranalysis5, each of which imports the previous one. They don't seem particularly big, and they all run very fast. Do we know why they were split, or is it lost to time? (I checked the repo, but they were added 18 years in roughly the same shape as they are now).
Last updated: Feb 04 2023 at 21:02 UTC