src/HOL/Lambda/InductTermi.thy
changeset 24440 27dcdcff5ce4
parent 23750 a1db5f819d00
child 25972 94b15338da8d