src/HOL/Partial_Function.thy
changeset 61456 b521b8b400f7
parent 60758 d8d85a8172b5
child 61566 c3d6e570ccef