src/HOL/RealVector.thy
changeset 31577 ce3721fa1e17
parent 31494 1ba61c7b129f
child 31564 d2abf6f6f619