src/HOL/Fun.thy
changeset 26690 e30b8d500c7d
parent 26588 d83271bfaba5
child 27106 ff27dc6e7d05