--- a/src/HOL/Calculation.thy Tue Sep 21 17:28:02 1999 +0200
+++ b/src/HOL/Calculation.thy Tue Sep 21 17:28:33 1999 +0200
@@ -17,6 +17,12 @@
theorems [trans] = dvd_trans; (* dvd dvd dvd *)
+theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"; (* ~= <= < *)
+ by (simp! add: order_less_le);
+
+theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *)
+ by (simp! add: order_less_le);
+
theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *)
by (rule order_less_asym);