src/HOL/Fun_Def_Base.thy
changeset 74056 fb8d5c0133c9
parent 69605 a96320074298