src/HOL/Fun_Def.thy
changeset 58299 30ab8289f0e1
parent 58002 0ed1e999a0fb
child 58305 57752a91eec4