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