src/HOL/Lambda/InductTermi.thy
changeset 23555 16e5fd18905c
parent 22271 51a80e238b29
child 23750 a1db5f819d00