src/HOL/Analysis/Product_Vector.thy
changeset 69846 e02e3763e7a4
parent 69541 d466e0a639e4
child 70136 f03a01a18c6e
equal deleted inserted replaced
69845:d28e8199dcb9 69846:e02e3763e7a4