src/HOL/Analysis/Inner_Product.thy
changeset 65083 9a0e34edfad1
parent 65064 a4abec71279a
child 65513 587433a18053