HOL.Partial_Function