src/HOL/Induct/Com.thy
changeset 29805 a5da150bd0ab
parent 26806 40b411ec05aa
child 32367 a508148f7c25