src/HOL/Analysis/Product_Vector.thy
changeset 69467 e8893c893241
parent 69260 0a9688695a1b
child 69511 4cc5e4a528f8