src/HOL/Proofs/Lambda/InductTermi.thy
changeset 79552 f1c754e60ea0
parent 67613 ce654b0e6d69