/src/HOL/Hyperreal/
drwxr-xr-x [up]
-rw-r--r-- 2003-07-11 14:12 +0200 9838 EvenOdd.ML
-rw-r--r-- 2003-07-11 14:12 +0200 419 EvenOdd.thy
-rw-r--r-- 2003-07-11 14:12 +0200 19515 ExtraThms2.ML
-rw-r--r-- 2003-07-11 14:12 +0200 21 ExtraThms2.thy
-rw-r--r-- 2003-07-11 14:12 +0200 2181 Fact.ML
-rw-r--r-- 2003-07-11 14:12 +0200 290 Fact.thy
-rw-r--r-- 2003-07-11 14:12 +0200 19424 Filter.ML
-rw-r--r-- 2003-07-11 14:12 +0200 1373 Filter.thy
-rw-r--r-- 2003-07-11 14:12 +0200 10234 HLog.ML
-rw-r--r-- 2003-07-11 14:12 +0200 479 HLog.thy
-rw-r--r-- 2003-07-11 14:12 +0200 8126 HRealAbs.ML
-rw-r--r-- 2003-07-11 14:12 +0200 414 HRealAbs.thy
-rw-r--r-- 2003-07-11 14:12 +0200 12021 HSeries.ML
-rw-r--r-- 2003-07-11 14:12 +0200 751 HSeries.thy
-rw-r--r-- 2003-07-11 14:12 +0200 29185 HTranscendental.ML
-rw-r--r-- 2003-07-11 14:12 +0200 735 HTranscendental.thy
-rw-r--r-- 2003-07-11 14:12 +0200 90 HyperArith.thy
-rw-r--r-- 2003-07-11 14:12 +0200 22450 HyperArith0.ML
-rw-r--r-- 2003-07-11 14:12 +0200 89 HyperArith0.thy
-rw-r--r-- 2003-07-11 14:12 +0200 23151 HyperBin.ML
-rw-r--r-- 2003-07-11 14:12 +0200 453 HyperBin.thy
-rw-r--r-- 2003-07-11 14:12 +0200 44238 HyperDef.ML
-rw-r--r-- 2003-07-11 14:12 +0200 2216 HyperDef.thy
-rw-r--r-- 2003-07-11 14:12 +0200 45708 HyperNat.ML
-rw-r--r-- 2003-07-11 14:12 +0200 2575 HyperNat.thy
-rw-r--r-- 2003-07-11 14:12 +0200 20137 HyperOrd.ML
-rw-r--r-- 2003-07-11 14:12 +0200 519 HyperOrd.thy
-rw-r--r-- 2003-07-11 14:12 +0200 19984 HyperPow.ML
-rw-r--r-- 2003-07-11 14:12 +0200 999 HyperPow.thy
-rw-r--r-- 2003-07-11 14:12 +0200 349 Hyperreal.thy
-rw-r--r-- 2003-07-11 14:12 +0200 10607 IntFloor.ML
-rw-r--r-- 2003-07-11 14:12 +0200 366 IntFloor.thy
-rw-r--r-- 2003-07-11 14:12 +0200 41690 Integration.ML
-rw-r--r-- 2003-07-11 14:12 +0200 2430 Integration.thy
-rw-r--r-- 2003-07-11 14:12 +0200 91647 Lim.ML
-rw-r--r-- 2003-07-11 14:12 +0200 2678 Lim.thy
-rw-r--r-- 2003-07-11 14:12 +0200 4692 Log.ML
-rw-r--r-- 2003-07-11 14:12 +0200 422 Log.thy
-rw-r--r-- 2003-07-11 14:12 +0200 27313 MacLaurin.ML
-rw-r--r-- 2003-07-11 14:12 +0200 172 MacLaurin.thy
-rw-r--r-- 2003-07-11 14:12 +0200 86591 NSA.ML
-rw-r--r-- 2003-07-11 14:12 +0200 1153 NSA.thy
-rw-r--r-- 2003-07-11 14:12 +0200 18003 NatStar.ML
-rw-r--r-- 2003-07-11 14:12 +0200 1795 NatStar.thy
-rw-r--r-- 2003-07-11 14:12 +0200 6709 NthRoot.ML
-rw-r--r-- 2003-07-11 14:12 +0200 254 NthRoot.thy
-rw-r--r-- 2003-07-11 14:12 +0200 44972 Poly.ML
-rw-r--r-- 2003-07-11 14:12 +0200 4803 Poly.thy
-rw-r--r-- 2003-07-11 14:12 +0200 1569 README.html
-rw-r--r-- 2003-07-11 14:12 +0200 50873 SEQ.ML
-rw-r--r-- 2003-07-11 14:12 +0200 2073 SEQ.thy
-rw-r--r-- 2003-07-11 14:12 +0200 22041 Series.ML
-rw-r--r-- 2003-07-11 14:12 +0200 641 Series.thy
-rw-r--r-- 2003-07-11 14:12 +0200 18026 Star.ML
-rw-r--r-- 2003-07-11 14:12 +0200 1461 Star.thy
-rw-r--r-- 2003-07-11 14:12 +0200 116009 Transcendental.ML
-rw-r--r-- 2003-07-11 14:12 +0200 1385 Transcendental.thy
-rw-r--r-- 2003-07-11 14:12 +0200 2765 fuf.ML
-rw-r--r-- 2003-07-11 14:12 +0200 1168 hypreal_arith.ML
-rw-r--r-- 2003-07-11 14:12 +0200 4269 hypreal_arith0.ML