src/HOL/Library/Poly_Mapping.thy
changeset 75721 9f540b73d665
parent 75455 91c16c5ad3e9
child 76484 defaa0b17424