src/HOL/Library/Poly_Mapping.thy
changeset 70720 99e24569cc1f
parent 70045 7b6add80e3a5
child 73655 26a1d66b9077