src/HOL/Library/Inner_Product.thy
changeset 63720 bcf2123d059a
parent 63589 58aab4745e85
child 63886 685fb01256af