src/HOL/Induct/Ordinals.thy
changeset 24389 9ddef2b1118a
parent 21404 eb85850d3eb7
child 36862 952b2b102a0a