src/HOL/Induct/Ordinals.thy
changeset 14024 213dcc39358f
parent 11649 dfb59b9954a6
child 14717 7d8d4c9b36fd