src/HOL/Library/Product_Vector.thy
changeset 54489 03ff4d1e6784
parent 53930 896b642f2aab
child 54779 d9edb711ef31