--- a/src/HOL/Ord.thy Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/Ord.thy Fri Feb 20 17:56:39 1998 +0100
@@ -45,4 +45,7 @@
order_antisym "[| x <= y; y <= x |] ==> x = y"
order_less_le "x < y = (x <= y & x ~= y)"
+axclass linorder < order
+ linorder_linear "x <= y | y <= x"
+
end