src/HOL/Fun_Def.thy
changeset 64342 53fb4a19fb98
parent 63654 f90e3926e627
child 64591 240a39af9ec4