src/HOL/Library/Mapping.thy
changeset 64597 1c252d8b6ca6
parent 63476 ff1d86b07751
child 66251 cd935b7cb3fb