src/HOL/Library/Poly_Mapping.thy
changeset 74610 87fc10f5826c
parent 73932 fd21b4a93043
child 75455 91c16c5ad3e9