# HG changeset patch
# User haftmann
# Date 1213988416 -7200
# Node ID a5373b60e66c714747abfb73f6806e27d48675f8
# Parent  2c42b1505f2577fa25969e5ab113eb2dd66dfced
moved Float.thy to Library

diff -r 2c42b1505f25 -r a5373b60e66c src/HOL/Complex/ROOT.ML
--- a/src/HOL/Complex/ROOT.ML	Fri Jun 20 20:03:13 2008 +0200
+++ b/src/HOL/Complex/ROOT.ML	Fri Jun 20 21:00:16 2008 +0200
@@ -5,5 +5,4 @@
 The Complex Numbers.
 *)
 
-no_document use_thys ["Infinite_Set", "Parity"];
-use_thys ["../Real/Float", "Complex_Main"];
+use_thy "Complex_Main";
diff -r 2c42b1505f25 -r a5373b60e66c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jun 20 20:03:13 2008 +0200
+++ b/src/HOL/IsaMakefile	Fri Jun 20 21:00:16 2008 +0200
@@ -167,9 +167,9 @@
 
 HOL-Complex: HOL $(OUT)/HOL-Complex
 
-$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML	\
+$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML                          \
   Library/Zorn.thy Library/Order_Relation.thy Real/ContNotDenum.thy	\
-  Real/float_arith.ML Real/Float.thy Real/Lubs.thy Real/PReal.thy	\
+  Real/float_arith.ML Real/Lubs.thy Real/PReal.thy                      \
   Real/RComplete.thy Real/Rational.thy Real/Real.thy Real/RealDef.thy	\
   Real/RealPow.thy Real/RealVector.thy Real/rat_arith.ML		\
   Real/real_arith.ML Hyperreal/StarDef.thy Hyperreal/Fact.thy		\
@@ -234,7 +234,7 @@
   Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
   Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
   Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
-  Library/Enum.thy
+  Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
 
diff -r 2c42b1505f25 -r a5373b60e66c src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Jun 20 20:03:13 2008 +0200
+++ b/src/HOL/Library/Library.thy	Fri Jun 20 21:00:16 2008 +0200
@@ -22,6 +22,7 @@
   Eval
   Eval_Witness
   Executable_Set
+  "../Real/Float"
   FuncSet
   GCD
   Imperative_HOL
diff -r 2c42b1505f25 -r a5373b60e66c src/HOL/Matrix/cplex/FloatSparseMatrix.thy
--- a/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Fri Jun 20 20:03:13 2008 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Fri Jun 20 21:00:16 2008 +0200
@@ -3,6 +3,8 @@
     Author:     Steven Obua
 *)
 
-theory FloatSparseMatrix imports Float SparseMatrix begin
+theory FloatSparseMatrix
+imports "../../Real/Float" SparseMatrix
+begin
 
 end