src/HOL/Induct/Ordinals.thy
changeset 32674 b629fbcc5313
parent 21404 eb85850d3eb7
child 36862 952b2b102a0a