src/HOL/Library/Poly_Mapping.thy
changeset 79931 f08e5a234c1b
parent 77955 c4677a6aae2c
child 80095 0f9cd1a5edbe