src/HOL/Induct/Comb.ML
changeset 3476 1be4fee7606b
parent 3207 fe79ad367d77
child 3724 f33e301a89f5