src/HOL/Matrix/cplex/FloatSparseMatrix.thy
changeset 16890 c4e5afaba440
parent 16784 92ff7c903585
child 27298 a5373b60e66c
     1.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Tue Jul 19 17:28:27 2005 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Tue Jul 19 17:28:37 2005 +0200
     1.3 @@ -3,6 +3,6 @@
     1.4      Author:     Steven Obua
     1.5  *)
     1.6  
     1.7 -theory FloatSparseMatrix = Float + SparseMatrix:
     1.8 +theory FloatSparseMatrix imports Float SparseMatrix begin
     1.9  
    1.10  end