/src/HOL/Real/
drwxr-xr-x [up]
drwxr-xr-x HahnBanach
drwxr-xr-x document
-rw-r--r-- 2006-07-26 00:44 +0200 22888 ContNotDenum.thy
-rw-r--r-- 2006-07-26 00:44 +0200 29273 Ferrante_Rackoff.thy
-rw-r--r-- 2006-07-26 00:44 +0200 13784 Float.ML
-rw-r--r-- 2006-07-26 00:44 +0200 16528 Float.thy
-rw-r--r-- 2006-07-26 00:44 +0200 2702 Lubs.thy
-rw-r--r-- 2006-07-26 00:44 +0200 44751 PReal.thy
-rw-r--r-- 2006-07-26 00:44 +0200 39994 RComplete.thy
-rw-r--r-- 2006-07-26 00:44 +0200 271 ROOT.ML
-rw-r--r-- 2006-07-26 00:44 +0200 15646 Rational.thy
-rw-r--r-- 2006-07-26 00:44 +0200 73 Real.thy
-rw-r--r-- 2006-07-26 00:44 +0200 33140 RealDef.thy
-rw-r--r-- 2006-07-26 00:44 +0200 8120 RealPow.thy
-rw-r--r-- 2006-07-26 00:44 +0200 4865 ferrante_rackoff.ML
-rw-r--r-- 2006-07-26 00:44 +0200 38411 ferrante_rackoff_proof.ML
-rw-r--r-- 2006-07-26 00:44 +0200 1896 rat_arith.ML
-rw-r--r-- 2006-07-26 00:44 +0200 7277 real_arith.ML