src/HOL/Induct/Comb.thy
changeset 13049 ce180e5b7fa0
parent 11359 29f8b00d7e1f
child 13075 d3e1d554cd6d