src/HOL/Induct/Comb.ML
changeset 3462 3472fa00b1d4
parent 3207 fe79ad367d77
child 3724 f33e301a89f5
equal deleted inserted replaced
3461:7bf1e7c40a0c 3462:3472fa00b1d4