added Real/Hyperreal
authorpaulson
Fri Nov 27 13:13:22 1998 +0100 (1998-11-27)
changeset 59802e9314c07146
parent 5979 11cbf236ca16
child 5981 ec5c3d17969f
added Real/Hyperreal
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Fri Nov 27 11:24:27 1998 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 27 13:13:22 1998 +0100
     1.3 @@ -135,7 +135,9 @@
     1.4    Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
     1.5    Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
     1.6    Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
     1.7 -  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML
     1.8 +  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
     1.9 +  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
    1.10 +  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy Real/Hyperreal/ROOT.ML
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL Real
    1.12  
    1.13