diff -r a681d3df1a39 -r a81ea5d3dd41 src/HOL/Hyperreal/HyperOrd.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HyperOrd.thy	Sat Dec 30 22:03:47 2000 +0100
@@ -0,0 +1,15 @@
+(*  Title:	 Real/Hyperreal/HyperOrd.thy
+    Author:      Jacques D. Fleuriot
+    Copyright:   2000 University of Edinburgh
+    Description: Type "hypreal" is a linear order and also 
+                 satisfies plus_ac0: + is an AC-operator with zero
+*)
+
+HyperOrd = HyperDef +
+
+instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le)
+instance hypreal :: linorder (hypreal_le_linear)
+
+instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left)
+
+end