src/HOL/Fun.thy
changeset 38795 848be46708dc
parent 38620 b40524b74f77
child 39074 211e4f6aad63