src/HOL/Analysis/Inner_Product.thy
changeset 66230 ae814012b95f
parent 65513 587433a18053
child 66486 ffaaa83543b2