src/HOL/Analysis/Product_Vector.thy
changeset 69517 dc20f278e8f3
parent 69511 4cc5e4a528f8
child 69541 d466e0a639e4