src/HOL/Library/Poly_Mapping.thy
changeset 77714 be0b9396604e
parent 76987 4c275405faae
child 77955 c4677a6aae2c