src/HOL/Induct/Com.thy
changeset 28820 95dd21624c6c
parent 26806 40b411ec05aa
child 32367 a508148f7c25