/src/HOL/Hyperreal/
drwxr-xr-x [up]
-rw-r--r-- 2003-12-19 10:38 +0100 9838 EvenOdd.ML
-rw-r--r-- 2003-12-19 10:38 +0100 419 EvenOdd.thy
-rw-r--r-- 2003-12-19 10:38 +0100 2181 Fact.ML
-rw-r--r-- 2003-12-19 10:38 +0100 290 Fact.thy
-rw-r--r-- 2003-12-19 10:38 +0100 19424 Filter.ML
-rw-r--r-- 2003-12-19 10:38 +0100 1373 Filter.thy
-rw-r--r-- 2003-12-19 10:38 +0100 10233 HLog.ML
-rw-r--r-- 2003-12-19 10:38 +0100 479 HLog.thy
-rw-r--r-- 2003-12-19 10:38 +0100 7814 HRealAbs.ML
-rw-r--r-- 2003-12-19 10:38 +0100 348 HRealAbs.thy
-rw-r--r-- 2003-12-19 10:38 +0100 12021 HSeries.ML
-rw-r--r-- 2003-12-19 10:38 +0100 751 HSeries.thy
-rw-r--r-- 2003-12-19 10:38 +0100 29185 HTranscendental.ML
-rw-r--r-- 2003-12-19 10:38 +0100 735 HTranscendental.thy
-rw-r--r-- 2003-12-19 10:38 +0100 90 HyperArith.thy
-rw-r--r-- 2003-12-19 10:38 +0100 21639 HyperArith0.ML
-rw-r--r-- 2003-12-19 10:38 +0100 89 HyperArith0.thy
-rw-r--r-- 2003-12-19 10:38 +0100 23363 HyperBin.ML
-rw-r--r-- 2003-12-19 10:38 +0100 453 HyperBin.thy
-rw-r--r-- 2003-12-19 10:38 +0100 49670 HyperDef.thy
-rw-r--r-- 2003-12-19 10:38 +0100 46434 HyperNat.ML
-rw-r--r-- 2003-12-19 10:38 +0100 2575 HyperNat.thy
-rw-r--r-- 2003-12-19 10:38 +0100 18607 HyperOrd.thy
-rw-r--r-- 2003-12-19 10:38 +0100 20561 HyperPow.ML
-rw-r--r-- 2003-12-19 10:38 +0100 999 HyperPow.thy
-rw-r--r-- 2003-12-19 10:38 +0100 349 Hyperreal.thy
-rw-r--r-- 2003-12-19 10:38 +0100 10607 IntFloor.ML
-rw-r--r-- 2003-12-19 10:38 +0100 366 IntFloor.thy
-rw-r--r-- 2003-12-19 10:38 +0100 41738 Integration.ML
-rw-r--r-- 2003-12-19 10:38 +0100 2430 Integration.thy
-rw-r--r-- 2003-12-19 10:38 +0100 91549 Lim.ML
-rw-r--r-- 2003-12-19 10:38 +0100 2680 Lim.thy
-rw-r--r-- 2003-12-19 10:38 +0100 4692 Log.ML
-rw-r--r-- 2003-12-19 10:38 +0100 422 Log.thy
-rw-r--r-- 2003-12-19 10:38 +0100 27316 MacLaurin.ML
-rw-r--r-- 2003-12-19 10:38 +0100 172 MacLaurin.thy
-rw-r--r-- 2003-12-19 10:38 +0100 88849 NSA.ML
-rw-r--r-- 2003-12-19 10:38 +0100 1153 NSA.thy
-rw-r--r-- 2003-12-19 10:38 +0100 18406 NatStar.ML
-rw-r--r-- 2003-12-19 10:38 +0100 1795 NatStar.thy
-rw-r--r-- 2003-12-19 10:38 +0100 6630 NthRoot.ML
-rw-r--r-- 2003-12-19 10:38 +0100 251 NthRoot.thy
-rw-r--r-- 2003-12-19 10:38 +0100 44995 Poly.ML
-rw-r--r-- 2003-12-19 10:38 +0100 4803 Poly.thy
-rw-r--r-- 2003-12-19 10:38 +0100 1569 README.html
-rw-r--r-- 2003-12-19 10:38 +0100 50902 SEQ.ML
-rw-r--r-- 2003-12-19 10:38 +0100 2073 SEQ.thy
-rw-r--r-- 2003-12-19 10:38 +0100 21977 Series.ML
-rw-r--r-- 2003-12-19 10:38 +0100 641 Series.thy
-rw-r--r-- 2003-12-19 10:38 +0100 18048 Star.ML
-rw-r--r-- 2003-12-19 10:38 +0100 1461 Star.thy
-rw-r--r-- 2003-12-19 10:38 +0100 117029 Transcendental.ML
-rw-r--r-- 2003-12-19 10:38 +0100 1385 Transcendental.thy
-rw-r--r-- 2003-12-19 10:38 +0100 2719 fuf.ML
-rw-r--r-- 2003-12-19 10:38 +0100 1168 hypreal_arith.ML
-rw-r--r-- 2003-12-19 10:38 +0100 4269 hypreal_arith0.ML