src/HOL/Cardinals/Ordinal_Arithmetic.thy
changeset 78951 c8c40e11c907
parent 76948 f33df7529fed
child 80914 d97fdabd9e2b