# HG changeset patch
# User huffman
# Date 1126821213 -7200
# Node ID 72325ec8fd8e908525417182967287f191f737af
# Parent  e8d6ed3aacfeaf84df98883624391942c02c7c9a
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy

diff -r e8d6ed3aacfe -r 72325ec8fd8e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 15 23:46:22 2005 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 15 23:53:33 2005 +0200
@@ -146,7 +146,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/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			\