src/HOL/Induct/Com.thy
changeset 7333 6cb15c6f1d9f
parent 5184 9b8547a9496a
child 10759 994877ee68cb