src/HOL/Library/Poly_Mapping.thy
changeset 75458 4117491aa7fe
parent 75455 91c16c5ad3e9
child 76484 defaa0b17424