src/HOL/Analysis/Product_Vector.thy
changeset 65321 2b1cd063e0b2
parent 63972 c98d1dd7eba1
child 66453 cc19f7ca2ed6