--- 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";
--- 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
--- 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
--- 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