# HG changeset patch
# User wenzelm
# Date 930751206 -7200
# Node ID 6c8bf18f9da9921b449aef3af22179f3e1d3cf52
# Parent  f80091bdc99206b3ecac50abfb171adbb3579642
antisym first;

diff -r f80091bdc992 -r 6c8bf18f9da9 src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Wed Jun 30 13:42:47 1999 +0200
+++ b/src/HOL/Calculation.thy	Wed Jun 30 16:00:06 1999 +0200
@@ -7,22 +7,22 @@
 
 theory Calculation = Int:;
 
+theorems [trans] = Ord.order_antisym;                   (*  <= <= =  *)
 theorems [trans] = Ord.order_trans;                     (*  <= <= <= *)
 theorems [trans] = Ord.order_less_trans;                (*  <  <  <  *)
 theorems [trans] = Ord.order_le_less_trans;             (*  <= <  <  *)
 theorems [trans] = Ord.order_less_le_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[with y z]);
 
-theorem [trans]: "[| x = y; y <= z |] ==> x <= z";
+theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	(*  =  <= <= *)
   by (rule HOL.ssubst[with x y]);
 
-theorem [trans]: "[| x < y; y = z |] ==> x < z";
+theorem [trans]: "[| x < y; y = z |] ==> x < z";	(*  <  =  <  *)
   by (rule HOL.subst[with y z]);
 
-theorem [trans]: "[| x = y; y < z |] ==> x < z";
+theorem [trans]: "[| x = y; y < z |] ==> x < z";	(*  =  <  <  *)
   by (rule HOL.ssubst[with x y]);
 
 theorems [trans] = HOL.subst[COMP swap_prems_rl];       (*  x  =  x  *)