HOL
HOL copied to clipboard
Move real-related materials out of `iterateTheory`
Hi,
This PR intends to make the iterateTheory a more fundamental theory without theorems about real numbers. The theory file is now moved to src/pred_set/src/more_theories, while the previous real-related materials of iterateTheory are moved into the existing real_sigmaTheory. This introduced a small incompatibility which can be fixed by opening real_sigmaTheory in addition to iterateTheory.
This changes paves the way for the abstract algebra materials to open iterateTheory for doing ring arithmetics (sum), etc. without having realTheory in ancestry, thus is important for some future work (on algebra materials).
--Chun