src/HOL/Library/Product_Vector.thy
changeset 55977 ec4830499634
parent 54890 cb892d835803
child 56181 2aa0b19e74f3