src/HOL/Lambda/InductTermi.thy
changeset 33556 cba22e2999d5
parent 26806 40b411ec05aa
child 36862 952b2b102a0a