src/HOL/Real/Real.thy

--- a/src/HOL/Real/Real.thy	Tue Aug 24 11:50:58 1999 +0200
+++ b/src/HOL/Real/Real.thy	Tue Aug 24 11:54:13 1999 +0200
@@ -1,14 +1,2 @@
-(*  Title:       Real/Real.thy
-    ID          : $Id$
-    Author:      Lawrence C. Paulson
-                 Jacques D. Fleuriot
-    Copyright:   1998  University of Cambridge
-    Description: Type "real" is a linear order
-*)
 
-Real = RealDef +
-
-instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
-instance real :: linorder (real_le_linear)
-
-end
+Real = RComplete