src/HOL/Library/Inner_Product.thy
changeset 60720 8c99fa3b7c44
parent 60679 ade12ef2773c
child 61518 ff12606337e9
equal deleted inserted replaced
60719:b6713e04889e 60720:8c99fa3b7c44