src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 70245 8feae28e5c44
parent 69276 3d954183b707
child 75624 22d1c5f2b9f4
equal deleted inserted replaced
70237:7e9269c188d6 70245:8feae28e5c44