src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 75052 9e1d486e2d9f
parent 69276 3d954183b707
child 75624 22d1c5f2b9f4
equal deleted inserted replaced
75051:1a8f6cb5efd6 75052:9e1d486e2d9f