src/HOL/Induct/Comb.ML
changeset 13049 ce180e5b7fa0
parent 11359 29f8b00d7e1f