src/HOL/Analysis/Inner_Product.thy
changeset 69554 4d4aedf9e57f
parent 69513 42e08052dae8
child 69597 ff784d5a5bfb
equal deleted inserted replaced
69553:2c2e2b3e19b7 69554:4d4aedf9e57f