src/HOL/Analysis/Product_Vector.thy
changeset 69554 4d4aedf9e57f
parent 69541 d466e0a639e4
child 70136 f03a01a18c6e