src/HOL/Induct/Comb.thy
changeset 78600 afb83ba8d24c
parent 76987 4c275405faae
child 80914 d97fdabd9e2b