src/HOL/Fun_Def_Base.thy
changeset 75168 ff60b4acd6dd
parent 69605 a96320074298