src/HOL/Fun.thy
changeset 82595 c0587d661ea8
parent 82395 918c50e0447e
child 82802 547335b41005