search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

Cardinal_ZF in ROOT ? #19

Closed CoghettoR closed 2 years ago

CoghettoR commented 2 years ago

Cardinal_ZF is used in the GROUP_ZF_4 theory and it appears in the pdf documents thanks to its dependency on GROUP_ZF_4. It is also used in Topology_ZF_examples

Would adding Cardinal_ZF in the ROOT file be a good idea?

SKolodynski commented 2 years ago

Yes, it should be there, right after func_ZF_1 as on the isarmathlib.org site. The way it is now it shows up in the proof document in a wrong place. Thank you for pointing this out, I will correct that on the next release.