src/HOL/Induct/Com.thy
changeset 24406 d96eb21fc1bc
parent 24178 4ff1dc2aa18d
child 24824 b7866aea0815