src/HOL/Cardinals/Ordinal_Arithmetic.thy
changeset 55719 cdddd073bff8
parent 55466 786edc984c98
child 55931 62156e694f3d