add Real/RealVector.thy
authorhuffman
Tue Sep 19 05:54:17 2006 +0200 (2006-09-19)
changeset 20583d96e19dd580f
parent 20582 ebd0e03c6a9b
child 20584 60b1d52a455d
add Real/RealVector.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 18 19:40:14 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 19 05:54:17 2006 +0200
     1.3 @@ -169,7 +169,8 @@
     1.4    Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/Float.ML			\
     1.5    Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy		\
     1.6    Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy			\
     1.7 -  Real/RealPow.thy Real/document/root.tex Real/ferrante_rackoff_proof.ML	\
     1.8 +  Real/RealPow.thy Real/RealVector.thy Real/document/root.tex                   \
     1.9 +  Real/ferrante_rackoff_proof.ML	                                        \
    1.10    Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML			\
    1.11    Hyperreal/StarDef.thy Hyperreal/StarClasses.thy				\
    1.12    Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\