src/HOL/Inductive.thy
changeset 20977 dbf1eca9b34e
parent 20604 9dba9c7872c9
child 21018 e6b8d6784792