/src/HOL/Real/
drwxr-xr-x [up]
drwxr-xr-x HahnBanach
-rw-r--r-- 2007-05-14 20:14 +0200 22915 ContNotDenum.thy
-rw-r--r-- 2007-05-14 20:14 +0200 29302 Ferrante_Rackoff.thy
-rw-r--r-- 2007-05-14 20:14 +0200 16436 Float.thy
-rw-r--r-- 2007-05-14 20:14 +0200 2786 Lubs.thy
-rw-r--r-- 2007-05-14 20:14 +0200 44582 PReal.thy
-rw-r--r-- 2007-05-14 20:14 +0200 39831 RComplete.thy
-rw-r--r-- 2007-05-14 20:14 +0200 271 ROOT.ML
-rw-r--r-- 2007-05-14 20:14 +0200 16033 Rational.thy
-rw-r--r-- 2007-05-14 20:14 +0200 84 Real.thy
-rw-r--r-- 2007-05-14 20:14 +0200 31115 RealDef.thy
-rw-r--r-- 2007-05-14 20:14 +0200 8950 RealPow.thy
-rw-r--r-- 2007-05-14 20:14 +0200 23869 RealVector.thy
-rw-r--r-- 2007-05-14 20:14 +0200 4628 ferrante_rackoff.ML
-rw-r--r-- 2007-05-14 20:14 +0200 38239 ferrante_rackoff_proof.ML
-rw-r--r-- 2007-05-14 20:14 +0200 6269 float_arith.ML
-rw-r--r-- 2007-05-14 20:14 +0200 2130 rat_arith.ML
-rw-r--r-- 2007-05-14 20:14 +0200 6974 real_arith.ML