src/HOL/Analysis/Product_Vector.thy
changeset 75866 9eeed5c424f9
parent 74475 409ca22dee4c
child 77228 8c093a4b8ccf