src/HOL/Inductive.thy
changeset 36800 59b50c691b75
parent 35115 446c5063e4fd
child 37390 8781d80026fc