src/HOL/Lambda/InductTermi.thy
changeset 8874 3242637f668c
parent 5717 0d28dbe484b6
child 9102 c7ba07e3bbe8