src/HOL/Fun_Def_Base.thy
changeset 71160 625df1eb7873
parent 69605 a96320074298
equal deleted inserted replaced
71159:6b03ce9b02c7 71160:625df1eb7873