src/HOL/Cardinals/Cardinal_Arithmetic.thy
changeset 57978 8f4a332500e4
parent 55851 3d40cf74726c
child 58127 b7cab82f488e