src/HOL/Fun_Def_Base.thy
changeset 81344 1b9ea66810ff
parent 69605 a96320074298
equal deleted inserted replaced
81343:b5b0c398cdec 81344:1b9ea66810ff