src/HOL/Library/Inner_Product.thy
changeset 60806 622d45ca75ee
parent 60679 ade12ef2773c
child 61518 ff12606337e9