src/HOL/Induct/Com.thy
changeset 24406 d96eb21fc1bc
parent 24178 4ff1dc2aa18d
child 24824 b7866aea0815
equal deleted inserted replaced
24405:30887caeba62 24406:d96eb21fc1bc