src/HOL/Library/Poly_Mapping.thy
changeset 78209 50c5be88ad59
parent 77955 c4677a6aae2c
child 80095 0f9cd1a5edbe