src/HOL/Analysis/Inner_Product.thy
changeset 70131 c6e1a4806f49
parent 69674 fc252acb7100
child 70136 f03a01a18c6e