src/HOL/Tools/Function/partial_function.ML
changeset 52583 0a7240d88e09
parent 52521 a1c4f586e372
child 52727 ce51d6eb8f3d