src/HOL/Fun_Def.thy
changeset 58846 98c03412079b
parent 58826 2ed2eaabe3df
child 58889 5b7a9633cfa8