# HG changeset patch
# User wenzelm
# Date 934230327 -7200
# Node ID 6fcaf006cc4009257bad3fce51e5a866920ea511
# Parent  59b9b7aec3c57fd7ba1023ea5ec690672559f309
added asym rule;

diff -r 59b9b7aec3c5 -r 6fcaf006cc40 src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Mon Aug 09 22:23:07 1999 +0200
+++ b/src/HOL/Calculation.thy	Mon Aug 09 22:25:27 1999 +0200
@@ -9,30 +9,33 @@
 theory Calculation = Int:;
 
 
-theorems [trans] = HOL.ssubst;                          (*  =  x  x  *)
-theorems [trans] = HOL.subst[COMP swap_prems_rl];       (*  x  =  x  *)
+theorems [trans] = HOL.ssubst;                              (*  =  x  x  *)
+theorems [trans] = HOL.subst[COMP swap_prems_rl];           (*  x  =  x  *)
 
-theorems [trans] = Divides.dvd_trans;                   (* dvd dvd dvd *)
+theorems [trans] = Divides.dvd_trans;                       (* dvd dvd dvd *)
+
+theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P";   (*  <  >  P  *)
+  by (rule Ord.order_less_asym);
 
-theorems [trans] = Ord.order_less_trans;                (*  <  <  <  *)
-theorems [trans] = Ord.order_le_less_trans;             (*  <= <  <  *)
-theorems [trans] = Ord.order_less_le_trans;             (*  <  <= <  *)
-theorems [trans] = Ord.order_trans;                     (*  <= <= <= *)
-theorems [trans] = Ord.order_antisym;                   (*  <= <= =  *)
+theorems [trans] = Ord.order_less_trans;                    (*  <  <  <  *)
+theorems [trans] = Ord.order_le_less_trans;                 (*  <= <  <  *)
+theorems [trans] = Ord.order_less_le_trans;                 (*  <  <= <  *)
+theorems [trans] = Ord.order_trans;                         (*  <= <= <= *)
+theorems [trans] = Ord.order_antisym;                       (*  <= >= =  *)
 
-theorem [trans]: "[| x <= y; y = z |] ==> x <= z";	(*  <= =  <= *)
+theorem [trans]: "[| x <= y; y = z |] ==> x <= z";	    (*  <= =  <= *)
   by (rule HOL.subst);
 
-theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	(*  =  <= <= *)
+theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	    (*  =  <= <= *)
   by (rule HOL.ssubst);
 
-theorem [trans]: "[| x < y; y = z |] ==> x < z";	(*  <  =  <  *)
+theorem [trans]: "[| x < y; y = z |] ==> x < z";	    (*  <  =  <  *)
   by (rule HOL.subst);
 
-theorem [trans]: "[| x = y; y < z |] ==> x < z";	(*  =  <  <  *)
+theorem [trans]: "[| x = y; y < z |] ==> x < z";	    (*  =  <  <  *)
   by (rule HOL.ssubst);
 
-theorems [trans] = HOL.trans                            (*  =  =  =  *)
+theorems [trans] = HOL.trans                                (*  =  =  =  *)
 
 
 end;