src/HOL/Induct/Com.thy
changeset 28741 1b257449f804
parent 26806 40b411ec05aa
child 32367 a508148f7c25