src/HOL/Fun.thy
changeset 5648 fe887910e32e
parent 5608 a82a038a3e7a
child 5852 4d7320490be4