src/HOL/Library/Product_Vector.thy
changeset 63243 1bc6816fd525
parent 63040 eb4ddd18d635