src/HOL/Library/Product_Vector.thy
changeset 61976 3a27957ac658
parent 61973 0c7e865fa7cb
child 62101 26c0a70f78a3