src/HOL/Fun.thy
changeset 82518 da14e77a48b2
parent 82395 918c50e0447e