src/HOL/Induct/Com.thy
changeset 28401 d5f39173444c
parent 26806 40b411ec05aa
child 32367 a508148f7c25