--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Matrix/cplex/ROOT.ML Wed Jul 13 12:24:39 2005 +0200 @@ -0,0 +1,5 @@ +(* Title: HOL/Matrix/cplex/ROOT.ML + ID: $Id$ +*) + +(*use_thy "Cplex";*) \ No newline at end of file