src/HOL/Analysis/Product_Vector.thy
changeset 74913 c2a2be496f35
parent 74475 409ca22dee4c
child 77228 8c093a4b8ccf