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