src/HOL/Inductive.thy
changeset 24710 141df8b68f63
parent 24699 c6674504103f
child 24720 4d2f2e375fa1