src/HOL/Fun_Def_Base.thy
changeset 75168 ff60b4acd6dd
parent 69605 a96320074298
equal deleted inserted replaced
75167:0a300751fdf5 75168:ff60b4acd6dd