src/HOL/Fun.thy
changeset 82388 f1ff9123c62a
parent 82201 b1af763166f4
child 82390 558bff66be22