src/HOL/Analysis/Inner_Product.thy
changeset 68325 57e4bd1e2e18
parent 68073 fad29d2a17a5
child 68499 d4312962161a