src/HOL/Fun.thy
changeset 37219 7c5311e54ea4
parent 36176 3fe7e97ccca8
child 37751 89e16802b6cc