src/HOL/Fun.thy
changeset 81351 95cb584cb777
parent 81182 fc5066122e68
child 81563 c4c983c5c7f2