HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Move real-related materials out of `iterateTheory`

Open binghe opened this issue 1 year ago • 0 comments

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

binghe avatar May 24 '24 10:05 binghe