src/HOL/Induct/Com.thy
changeset 7990 0a604b2fc2b1
parent 5184 9b8547a9496a
child 10759 994877ee68cb