src/HOL/Induct/Ordinals.thy
changeset 21234 fb84ab52f23b
parent 19736 d8d0f8f51d69
child 21404 eb85850d3eb7