src/HOL/Lambda/InductTermi.thy
changeset 31106 9a1178204dc0
parent 26806 40b411ec05aa
child 36862 952b2b102a0a