src/HOL/Cardinals/Ordinal_Arithmetic.thy
changeset 55106 080c0006e917
parent 55023 38db7814481d
child 55102 761e40ce91bc