src/HOL/Library/Poly_Mapping.thy
changeset 71988 ace45a11a45e
parent 70045 7b6add80e3a5
child 73655 26a1d66b9077