src/HOL/Fun_Def_Base.thy
changeset 64948 e655d965307c
parent 60758 d8d85a8172b5
child 69605 a96320074298
equal deleted inserted replaced
64947:f6ad52152040 64948:e655d965307c