src/HOL/Calculation.thy
changeset 7561 ff8dbd0589aa
parent 7381 1bd8633e8f90
child 7657 dbbf7721126e
     1.1 --- a/src/HOL/Calculation.thy	Tue Sep 21 17:28:02 1999 +0200
     1.2 +++ b/src/HOL/Calculation.thy	Tue Sep 21 17:28:33 1999 +0200
     1.3 @@ -17,6 +17,12 @@
     1.4  
     1.5  theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)
     1.6  
     1.7 +theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y";     (*  ~=  <=  < *)
     1.8 +  by (simp! add: order_less_le);
     1.9 +
    1.10 +theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";     (*  <=  ~=  < *)
    1.11 +  by (simp! add: order_less_le);
    1.12 +
    1.13  theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P";   (*  <  >  P  *)
    1.14    by (rule order_less_asym);
    1.15