src/HOL/Fun.thy
changeset 26840 ec46381f149d
parent 26588 d83271bfaba5
child 27106 ff27dc6e7d05