# HG changeset patch
# User wenzelm
# Date 1121786917 -7200
# Node ID c4e5afaba4407a882941acd37a60a9555a5ab7f9
# Parent  b50947fa958d278240ee7147bd4e6fbe6b144046
isatool fixheaders;

diff -r b50947fa958d -r c4e5afaba440 src/HOL/Matrix/cplex/Cplex.thy
--- a/src/HOL/Matrix/cplex/Cplex.thy	Tue Jul 19 17:28:27 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex.thy	Tue Jul 19 17:28:37 2005 +0200
@@ -5,7 +5,7 @@
 
 theory Cplex 
 imports FloatSparseMatrix
-files "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
+uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
 begin
 
 end
diff -r b50947fa958d -r c4e5afaba440 src/HOL/Matrix/cplex/FloatSparseMatrix.thy
--- a/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Tue Jul 19 17:28:27 2005 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Tue Jul 19 17:28:37 2005 +0200
@@ -3,6 +3,6 @@
     Author:     Steven Obua
 *)
 
-theory FloatSparseMatrix = Float + SparseMatrix:
+theory FloatSparseMatrix imports Float SparseMatrix begin
 
 end
diff -r b50947fa958d -r c4e5afaba440 src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Tue Jul 19 17:28:27 2005 +0200
+++ b/src/HOL/Real/Float.thy	Tue Jul 19 17:28:37 2005 +0200
@@ -3,7 +3,7 @@
     Author: Steven Obua
 *)
 
-theory Float = Real:
+theory Float imports Real begin
 
 constdefs  
   pow2 :: "int \<Rightarrow> real"