# HG changeset patch
# User wenzelm
# Date 1121786907 -7200
# Node ID b50947fa958d278240ee7147bd4e6fbe6b144046
# Parent  7cb4bcfa058e325720731868352c285992f615fd
with_path;

diff -r 7cb4bcfa058e -r b50947fa958d src/HOL/Matrix/ROOT.ML
--- a/src/HOL/Matrix/ROOT.ML	Tue Jul 19 17:24:09 2005 +0200
+++ b/src/HOL/Matrix/ROOT.ML	Tue Jul 19 17:28:27 2005 +0200
@@ -3,6 +3,4 @@
 *)
 
 use_thy "SparseMatrix";
-cd "cplex"; use_thy "MatrixLP"; cd "..";
-
-
+with_path "cplex" use_thy "MatrixLP";