src/HOL/Library/Product_Vector.thy
changeset 44489 6cddca146ca0
parent 44282 f0de18b62d63
child 44568 e6f291cb5810