src/HOL/Partial_Function.thy
changeset 62764 ff3b8e4079bd
parent 62390 842917225d56
child 63561 fba08009ff3e