src/HOL/Induct/Com.thy
changeset 36811 4ab4aa5bee1c
parent 32367 a508148f7c25
child 36862 952b2b102a0a