changeset 11096 | bedfd42db838 |
parent 11089 | 0f6f1cd500e5 |
child 11253 | caabb021ec0f |
--- 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