src/HOL/Library/Inner_Product.thy
changeset 53964 ac0e4ca891f9
parent 53938 eb93cca4589a
child 54230 b1d955791529