src/HOL/Fun.thy
changeset 5688 7f582495967c
parent 5608 a82a038a3e7a
child 5852 4d7320490be4