src/HOL/Library/Product_Vector.thy
changeset 51288 be7e9a675ec9
parent 51002 496013a6eb38
child 51478 270b21f3ae0a