src/HOL/Fun_Def.thy
changeset 63711 e4843a8a8b18
parent 63654 f90e3926e627
child 64591 240a39af9ec4