src/HOL/Analysis/Inner_Product.thy
changeset 67760 553d9ad7d679
parent 67399 eab6ce8368fa
child 67962 0acdcd8f4ba1
equal deleted inserted replaced
67759:56eba30e7b99 67760:553d9ad7d679