src/HOL/Fun_Def_Base.thy
changeset 76378 c0566b6f6ca8
parent 69605 a96320074298