src/HOL/Analysis/Product_Vector.thy
changeset 64065 40d440b75b00
parent 63972 c98d1dd7eba1
child 66453 cc19f7ca2ed6