src/HOL/Library/Product_Vector.thy
changeset 63735 fb0ae6b60491
parent 63040 eb4ddd18d635