src/HOL/Lambda/InductTermi.thy
changeset 8216 e4b3192dfefa
parent 5717 0d28dbe484b6
child 9102 c7ba07e3bbe8