src/HOL/Induct/Ordinals.thy
changeset 61434 46d6586eb04c
parent 60532 7fb5b7dc8332
child 63680 6e1e8b5abbfa