src/HOL/Analysis/Inner_Product.thy
changeset 82471 4e63872f3646
parent 81116 0fb1e2dd4122
child 82489 d35d355f7330
equal deleted inserted replaced
82469:1fa80133027d 82471:4e63872f3646