src/HOL/Partial_Function.thy
changeset 60976 0a8c719d8c1f
parent 60758 d8d85a8172b5
child 61566 c3d6e570ccef