/src/HOL/Real/
drwxr-xr-x [up]
drwxr-xr-x HahnBanach
-rw-r--r-- 2006-12-13 00:02 +0100 22915 ContNotDenum.thy
-rw-r--r-- 2006-12-13 00:02 +0100 29286 Ferrante_Rackoff.thy
-rw-r--r-- 2006-12-13 00:02 +0100 16393 Float.thy
-rw-r--r-- 2006-12-13 00:02 +0100 2786 Lubs.thy
-rw-r--r-- 2006-12-13 00:02 +0100 44413 PReal.thy
-rw-r--r-- 2006-12-13 00:02 +0100 39831 RComplete.thy
-rw-r--r-- 2006-12-13 00:02 +0100 271 ROOT.ML
-rw-r--r-- 2006-12-13 00:02 +0100 15915 Rational.thy
-rw-r--r-- 2006-12-13 00:02 +0100 84 Real.thy
-rw-r--r-- 2006-12-13 00:02 +0100 32726 RealDef.thy
-rw-r--r-- 2006-12-13 00:02 +0100 7470 RealPow.thy
-rw-r--r-- 2006-12-13 00:02 +0100 15659 RealVector.thy
-rw-r--r-- 2006-12-13 00:02 +0100 4593 ferrante_rackoff.ML
-rw-r--r-- 2006-12-13 00:02 +0100 38437 ferrante_rackoff_proof.ML
-rw-r--r-- 2006-12-13 00:02 +0100 13520 float.ML
-rw-r--r-- 2006-12-13 00:02 +0100 2003 rat_arith.ML
-rw-r--r-- 2006-12-13 00:02 +0100 7358 real_arith.ML