src/HOL/Analysis/Inner_Product.thy
changeset 64877 31e9920a0dc1
parent 64267 b9a1486e79be
child 65064 a4abec71279a
equal deleted inserted replaced
64876:65a247444100 64877:31e9920a0dc1