# HG changeset patch
# User huffman
# Date 1158638057 -7200
# Node ID d96e19dd580f645cf9dcc3f483fa53f11518f69e
# Parent  ebd0e03c6a9b1cecea6d70bed90ab0bba3acfe34
add Real/RealVector.thy

diff -r ebd0e03c6a9b -r d96e19dd580f 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			\