src/HOL/Fun_Def_Base.thy
changeset 76703 8fac11f7f0f4
parent 69605 a96320074298