src/HOL/Matrix/ROOT.ML
author haftmann
Mon, 05 Jul 2010 16:46:23 +0200
changeset 37719 271ecd4fb9f9
parent 32491 d5d8bea0cd94
child 37764 3489daf839d5
permissions -rw-r--r--
moved "open" operations from Heap.thy to Array.thy and Ref.thy

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