src/HOL/Matrix/ROOT.ML

complex_of_real abbreviates of_real::real=>complex;
cmod abbreviates norm::complex=>real;
removed several redundant lemmas

(*  Title:      HOL/Matrix/ROOT.ML
    ID:         $Id$
*)

use_thy "SparseMatrix";
with_path "cplex" use_thy "MatrixLP";