src/HOL/Matrix/ROOT.ML

move class perfect_space into RealVector.thy;
use not_open_singleton as perfect_space class axiom;
generalize some lemmas to class perfect_space;

use_thy "Cplex";