src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 73255 7e2a9a8c2b85
parent 69276 3d954183b707
child 75624 22d1c5f2b9f4