src/HOL/Fun_Def.thy
changeset 67051 e7e54a0b9197
parent 64591 240a39af9ec4
child 67443 3abf6a722518