src/HOL/Induct/Ordinals.thy
changeset 61087 1e36b5d021f2
parent 60532 7fb5b7dc8332
child 63680 6e1e8b5abbfa