src/HOL/Induct/Com.ML
changeset 12395 d6913de7655f
parent 10797 028d22926a41
child 12486 0ed8bdd883e0