src/HOL/Fun.thy
changeset 33571 3655e51f9958
parent 33057 764547b68538
child 33318 ddd97d9dfbfb