# HG changeset patch
# User wenzelm
# Date 937927713 -7200
# Node ID ff8dbd0589aa6215c19b003bf14db31115af202e
# Parent  19c3be2d285cae15ec1c05695fd01ec23f6a4156
added some ~= rules;

diff -r 19c3be2d285c -r ff8dbd0589aa src/HOL/Calculation.thy
--- 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);