src/HOL/Fun_Def_Base.thy
changeset 72884 50f18a822ee9
parent 69605 a96320074298