src/HOL/Fun.thy
changeset 77050 92509e4274eb
parent 76722 b1d57dd345e1
child 77138 c8597292cd41