src/HOL/Analysis/Product_Vector.thy
changeset 77011 3e48f8c6afc9
parent 74475 409ca22dee4c
child 77228 8c093a4b8ccf
equal deleted inserted replaced
77010:fead2b33acdc 77011:3e48f8c6afc9