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