src/HOL/IsaMakefile

   Real/Lubs.thy Real/rat_arith.ML						\
   Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
   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/StarDef.thy Hyperreal/StarClasses.thy				\
   Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
   Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML		\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy			\
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy					\
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy				\