src/HOL/Fun_Def_Base.thy
changeset 79662 dca6ea3b7a01
parent 69605 a96320074298
equal deleted inserted replaced
79661:2a9d8c74eb3c 79662:dca6ea3b7a01