src/HOL/Induct/Ordinals.thy
changeset 46148 04a8da7dcffc
parent 39246 9e58f0499f57
child 46914 c2ca2c3d23a6