src/HOL/Inductive.thy
changeset 32575 bf6c78d9f94c
parent 31949 3f933687fae9
child 32587 caa5ada96a00