src/HOL/Cardinals/Cardinal_Arithmetic.thy
changeset 62480 f2e8984adef7
parent 62390 842917225d56
child 63040 eb4ddd18d635