src/HOL/Induct/Com.ML
changeset 12887 d25b43743e10
parent 12486 0ed8bdd883e0