merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
authorhuffman
Thu Sep 15 23:53:33 2005 +0200 (2005-09-15)
changeset 1743072325ec8fd8e
parent 17429 e8d6ed3aacfe
child 17431 70311ad8bf11
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 15 23:46:22 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 15 23:53:33 2005 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4    Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
     1.5    Real/RealPow.thy Real/document/root.tex					\
     1.6    Real/Float.thy Real/Float.ML                                                  \
     1.7 -  Hyperreal/StarType.thy Hyperreal/Transfer.thy Hyperreal/StarClasses.thy	\
     1.8 +  Hyperreal/StarDef.thy Hyperreal/StarClasses.thy				\
     1.9    Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
    1.10    Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML		\
    1.11    Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy			\