src/HOL/Cardinals/Cardinal_Arithmetic.thy
changeset 79728 df4eb4b05ecd
parent 76946 5df58a471d9e