src/HOL/Cardinals/Ordinal_Arithmetic.thy
changeset 55914 c5b752d549e3
parent 55466 786edc984c98
child 55931 62156e694f3d
equal deleted inserted replaced
55913:c1409c103b77 55914:c5b752d549e3