src/HOL/Lambda/InductTermi.thy
changeset 9502 50ec59aff389
parent 9102 c7ba07e3bbe8
child 9716 9be481b4bc85