src/HOL/Analysis/Inner_Product.thy
changeset 68591 90381a0f5474
parent 68499 d4312962161a
child 68611 4bc4b5c0ccfc