src/HOL/Partial_Function.thy
changeset 40172 008dc2d2c395
parent 40107 374f3ef9f940
child 40252 029400b6c893