src/HOL/Induct/Comb.thy
changeset 9713 2c5b42311eb0
parent 9101 b643f4d7b9e9
child 11359 29f8b00d7e1f