src/HOL/Library/Product_Vector.thy
changeset 63540 f8652d0534fa
parent 63040 eb4ddd18d635