add Hyperreal dependencies
authorhuffman
Tue, 06 Sep 2005 23:14:10 +0200
changeset 17297 17256fe71aca
parent 17296 d0e0905d548e
child 17298 ad73fb6144cf
add Hyperreal dependencies
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 06 23:11:46 2005 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 06 23:14:10 2005 +0200
@@ -144,6 +144,7 @@
   Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
   Real/RealPow.thy Real/document/root.tex					\
   Real/Float.thy Real/Float.ML                                                  \
+  Hyperreal/StarType.thy Hyperreal/Transfer.thy Hyperreal/StarClasses.thy	\
   Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
   Hyperreal/Filter.thy Hyperreal/HSeries.thy					\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy			\