src/HOL/Library/Product_Vector.thy
changeset 35817 d8b8527102f5
parent 34110 4c113c744b86
child 36332 3ddb2bc07784
equal deleted inserted replaced
35816:2449e026483d 35817:d8b8527102f5