# HG changeset patch
# User wenzelm
# Date 981905514 -3600
# Node ID bedfd42db83865a518a16478a28e79d0e9e72e69
# Parent  2ffaf1e1e101a584a80ebf70414c2eecd49e2402
tuned trans rules;

diff -r 2ffaf1e1e101 -r bedfd42db838 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sun Feb 11 16:31:21 2001 +0100
+++ b/src/FOL/FOL.thy	Sun Feb 11 16:31:54 2001 +0100
@@ -88,8 +88,8 @@
   back_subst
   rev_mp
   mp
+  transitive
   trans
-  transitive
 
 lemmas [elim?] = sym
 
diff -r 2ffaf1e1e101 -r bedfd42db838 src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Sun Feb 11 16:31:21 2001 +0100
+++ b/src/HOL/Calculation.thy	Sun Feb 11 16:31:54 2001 +0100
@@ -154,7 +154,6 @@
 *}
 
 lemmas basic_trans_rules [trans] =
-  forw_subst
   order_less_subst2
   order_less_subst1
   order_le_less_subst2
@@ -167,6 +166,7 @@
   ord_eq_le_subst
   ord_less_eq_subst
   ord_eq_less_subst
+  forw_subst
   back_subst
   dvd_trans
   rev_mp
@@ -185,7 +185,7 @@
   ord_eq_le_trans
   ord_less_eq_trans
   ord_eq_less_trans
+  transitive
   trans
-  transitive
 
 end