src/HOL/Analysis/Inner_Product.thy
changeset 63991 0d8cd1f3c26d
parent 63971 da89140186e2
child 64267 b9a1486e79be