src/HOL/Induct/Com.ML
changeset 6538 d575fb1edabf
parent 6300 3815b5b095cb
child 10759 994877ee68cb