src/HOL/Cardinals/Cardinal_Arithmetic.thy
changeset 54643 57aefb80b639
parent 52634 7c4b56bac189
child 54473 8bee5ca99e63