moved Float.thy to Library
authorhaftmann
Fri Jun 20 21:00:16 2008 +0200 (2008-06-20)
changeset 27298a5373b60e66c
parent 27297 2c42b1505f25
child 27299 3447cd2e18e8
moved Float.thy to Library
src/HOL/Complex/ROOT.ML
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Matrix/cplex/FloatSparseMatrix.thy
     1.1 --- a/src/HOL/Complex/ROOT.ML	Fri Jun 20 20:03:13 2008 +0200
     1.2 +++ b/src/HOL/Complex/ROOT.ML	Fri Jun 20 21:00:16 2008 +0200
     1.3 @@ -5,5 +5,4 @@
     1.4  The Complex Numbers.
     1.5  *)
     1.6  
     1.7 -no_document use_thys ["Infinite_Set", "Parity"];
     1.8 -use_thys ["../Real/Float", "Complex_Main"];
     1.9 +use_thy "Complex_Main";
     2.1 --- a/src/HOL/IsaMakefile	Fri Jun 20 20:03:13 2008 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Jun 20 21:00:16 2008 +0200
     2.3 @@ -167,9 +167,9 @@
     2.4  
     2.5  HOL-Complex: HOL $(OUT)/HOL-Complex
     2.6  
     2.7 -$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML	\
     2.8 +$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML                          \
     2.9    Library/Zorn.thy Library/Order_Relation.thy Real/ContNotDenum.thy	\
    2.10 -  Real/float_arith.ML Real/Float.thy Real/Lubs.thy Real/PReal.thy	\
    2.11 +  Real/float_arith.ML Real/Lubs.thy Real/PReal.thy                      \
    2.12    Real/RComplete.thy Real/Rational.thy Real/Real.thy Real/RealDef.thy	\
    2.13    Real/RealPow.thy Real/RealVector.thy Real/rat_arith.ML		\
    2.14    Real/real_arith.ML Hyperreal/StarDef.thy Hyperreal/Fact.thy		\
    2.15 @@ -234,7 +234,7 @@
    2.16    Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
    2.17    Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
    2.18    Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
    2.19 -  Library/Enum.thy
    2.20 +  Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
    2.21  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    2.22  
    2.23  
     3.1 --- a/src/HOL/Library/Library.thy	Fri Jun 20 20:03:13 2008 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Fri Jun 20 21:00:16 2008 +0200
     3.3 @@ -22,6 +22,7 @@
     3.4    Eval
     3.5    Eval_Witness
     3.6    Executable_Set
     3.7 +  "../Real/Float"
     3.8    FuncSet
     3.9    GCD
    3.10    Imperative_HOL
     4.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Fri Jun 20 20:03:13 2008 +0200
     4.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Fri Jun 20 21:00:16 2008 +0200
     4.3 @@ -3,6 +3,8 @@
     4.4      Author:     Steven Obua
     4.5  *)
     4.6  
     4.7 -theory FloatSparseMatrix imports Float SparseMatrix begin
     4.8 +theory FloatSparseMatrix
     4.9 +imports "../../Real/Float" SparseMatrix
    4.10 +begin
    4.11  
    4.12  end