--- 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