src/HOL/Fun_Def.thy
changeset 60976 0a8c719d8c1f
parent 60758 d8d85a8172b5
child 61032 b57df8eecad6