src/HOL/Cardinals/Ordinal_Arithmetic.thy
changeset 57055 df3a26987a8d
parent 55932 68c5104d2204
child 58127 b7cab82f488e