src/HOL/Fun_Def_Base.thy
changeset 79604 0e8ac7db1f4d
parent 69605 a96320074298
equal deleted inserted replaced
79603:9f002cdb6b8d 79604:0e8ac7db1f4d