src/HOL/Induct/Ordinals.thy
changeset 61578 6623c81cb15a
parent 60532 7fb5b7dc8332
child 63680 6e1e8b5abbfa