src/HOL/Lambda/InductTermi.thy
changeset 18264 3b808e24667b
parent 18241 afdba6b3e383
child 18513 791b53bf4073