src/HOL/Induct/Com.thy
changeset 43074 8b566f0d226c
parent 41818 6d4c3ee8219d
child 44174 d1d79f0e1ea6