src/HOL/RealVector.thy
changeset 31563 ded2364d14d4
parent 31494 1ba61c7b129f
child 31564 d2abf6f6f619