src/HOL/Matrix/ROOT.ML
author haftmann
Mon, 08 Feb 2010 14:06:41 +0100
changeset 35032 7efe662e41b4
parent 32491 d5d8bea0cd94
child 37764 3489daf839d5
permissions -rw-r--r--
separate library theory for type classes combining lattices with various algebraic structures

use_thys ["SparseMatrix", "cplex/Cplex"];