src/HOL/Induct/Comb.ML
changeset 12655 b8c130dc46be
parent 11359 29f8b00d7e1f