src/HOL/Cardinals/Cardinal_Arithmetic.thy
changeset 83240 dfa14d921fd2
parent 76946 5df58a471d9e