src/HOL/Induct/Ordinals.thy
changeset 13545 fcdbd6cf5f9f
parent 11649 dfb59b9954a6
child 14717 7d8d4c9b36fd
equal deleted inserted replaced
13544:895994073bdf 13545:fcdbd6cf5f9f