src/HOL/RealVector.thy
changeset 44798 9900c0069ae6
parent 44571 bd91b77c4cd6
child 44937 22c0857b8aab
equal deleted inserted replaced
44797:e0da66339e47 44798:9900c0069ae6