src/HOL/Induct/Ordinals.thy
changeset 72369 694d0a315d0a
parent 63680 6e1e8b5abbfa
child 76063 24c9f56aa035
equal deleted inserted replaced
72368:b86d1e754e78 72369:694d0a315d0a