src/HOL/Induct/Ordinals.thy
changeset 62337 d3996d5873dd
parent 60532 7fb5b7dc8332
child 63680 6e1e8b5abbfa