src/HOL/Analysis/Product_Vector.thy
changeset 75155 0b6c43a87fa6
parent 74475 409ca22dee4c
child 77228 8c093a4b8ccf
equal deleted inserted replaced
75154:3b5aa38282bd 75155:0b6c43a87fa6