src/HOL/Induct/Com.ML
changeset 7990 0a604b2fc2b1
parent 6300 3815b5b095cb
child 10759 994877ee68cb