src/HOL/Partial_Function.thy
changeset 54010 5ac1495fed4e
parent 53949 021a8ef97f5f
child 54630 9061af4d5ebc