# HG changeset patch
# User wenzelm
# Date 930843747 -7200
# Node ID b123f5522ea1d022fd0ffca10a6f5db31da13d92
# Parent  b250da153b1e3c203691d2815bed5b7d7dacb719
tuned;

diff -r b250da153b1e -r b123f5522ea1 src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Thu Jul 01 17:41:16 1999 +0200
+++ b/src/HOL/Calculation.thy	Thu Jul 01 17:42:27 1999 +0200
@@ -2,33 +2,34 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Setup transitivity rules for calculational proofs.
+Setup transitivity rules for calculational proofs.  Note that in the
+list below later rules have priority.
 *)
 
 theory Calculation = Int:;
 
-theorems [trans] = Ord.order_antisym;                   (*  <= <= =  *)
-theorems [trans] = Ord.order_trans;                     (*  <= <= <= *)
+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] = 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";	(*  <= =  <= *)
-  by (rule HOL.subst[with y z]);
+  by (rule HOL.subst);
 
 theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	(*  =  <= <= *)
-  by (rule HOL.ssubst[with x y]);
+  by (rule HOL.ssubst);
 
 theorem [trans]: "[| x < y; y = z |] ==> x < z";	(*  <  =  <  *)
-  by (rule HOL.subst[with y z]);
+  by (rule HOL.subst);
 
 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  *)
-theorems [trans] = HOL.ssubst;                          (*  =  x  x  *)
-
-theorems [trans] = Divides.dvd_trans;                   (* dvd dvd dvd *)
+  by (rule HOL.ssubst);
 
 
 end;