src/HOL/Library/Mapping.thy
changeset 55400 1e8dd9cd320b
parent 54853 a435932a9f12
child 55466 786edc984c98