tuned trans rules;
authorwenzelm
Sun, 11 Feb 2001 16:31:54 +0100
changeset 11096 bedfd42db838
parent 11095 2ffaf1e1e101
child 11097 c1be9f2dff4c
tuned trans rules;
src/FOL/FOL.thy
src/HOL/Calculation.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
 
--- 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