src/HOL/Induct/Com.ML
changeset 7333 6cb15c6f1d9f
parent 6300 3815b5b095cb
child 10759 994877ee68cb