src/HOL/Fun.thy
changeset 26964 df1f238a05f7
parent 26588 d83271bfaba5
child 27106 ff27dc6e7d05