src/HOL/Induct/Com.thy
changeset 60162 645058aa9d6f
parent 59807 22bc39064290
child 60530 44f9873d6f6f