src/HOL/Lambda/InductTermi.thy
changeset 24434 c588ec4cf194
parent 23750 a1db5f819d00
child 25972 94b15338da8d