src/HOL/Inductive.thy
changeset 31904 a86896359ca4
parent 31784 bd3486c57ba3
child 31949 3f933687fae9