src/HOL/Library/Inner_Product.thy
changeset 30268 5af6ed62385b
parent 30067 84205156ca8a
child 30663 0b6aff7451b2