src/HOL/Fun.thy
changeset 33756 47b7c9e0bf6e
parent 33318 ddd97d9dfbfb
child 34101 d689f0b33047