src/HOL/Fun_Def_Base.thy
changeset 77128 f40c36ab154d
parent 69605 a96320074298
equal deleted inserted replaced
77127:a8f002720ebb 77128:f40c36ab154d