src/HOL/Analysis/Inner_Product.thy
changeset 69880 fe3c12990893
parent 69674 fc252acb7100
child 70136 f03a01a18c6e