src/HOL/Fun_Def_Base.thy
changeset 78206 f4f441edafca
parent 69605 a96320074298
equal deleted inserted replaced
78205:a40ae2df39ad 78206:f4f441edafca