src/HOL/Fun_Def.thy
changeset 58306 117ba6cbe414
parent 58305 57752a91eec4
child 58377 c6f93b8d2d8e