src/HOL/Analysis/Product_Vector.thy
changeset 74971 16eaa56f69f7
parent 74475 409ca22dee4c
child 77228 8c093a4b8ccf