src/HOL/Library/Inner_Product.thy
changeset 52342 df4fef9e15a7
parent 51642 400ec5ae7f8f
child 53015 a1119cf551e8
equal deleted inserted replaced
52341:fc66f7db2c0b 52342:df4fef9e15a7