src/HOL/Lambda/InductTermi.thy
changeset 20604 9dba9c7872c9
parent 18513 791b53bf4073
child 22271 51a80e238b29