src/HOL/Partial_Function.thy
changeset 44525 fbb777aec0d4
parent 43082 8d0c44de9773
child 45297 3c9f17d017bf