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