src/HOL/Analysis/Inner_Product.thy
changeset 68300 cd8ab1a7a286
parent 68073 fad29d2a17a5
child 68499 d4312962161a