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