src/HOL/Lambda/InductTermi.thy
changeset 23342 0261d2da0b1c
parent 22271 51a80e238b29
child 23750 a1db5f819d00