src/HOL/Induct/Com.thy
changeset 23942 079e99db59d7
parent 23746 a455e69c31cc
child 24178 4ff1dc2aa18d