src/HOL/Calculation.thy
changeset 11096 bedfd42db838
parent 11089 0f6f1cd500e5
child 11253 caabb021ec0f
equal deleted inserted replaced
11095:2ffaf1e1e101 11096:bedfd42db838
   152 text {*
   152 text {*
   153   Note that this list of rules is in reverse order of priorities.
   153   Note that this list of rules is in reverse order of priorities.
   154 *}
   154 *}
   155 
   155 
   156 lemmas basic_trans_rules [trans] =
   156 lemmas basic_trans_rules [trans] =
   157   forw_subst
       
   158   order_less_subst2
   157   order_less_subst2
   159   order_less_subst1
   158   order_less_subst1
   160   order_le_less_subst2
   159   order_le_less_subst2
   161   order_le_less_subst1
   160   order_le_less_subst1
   162   order_less_le_subst2
   161   order_less_le_subst2
   165   order_subst1
   164   order_subst1
   166   ord_le_eq_subst
   165   ord_le_eq_subst
   167   ord_eq_le_subst
   166   ord_eq_le_subst
   168   ord_less_eq_subst
   167   ord_less_eq_subst
   169   ord_eq_less_subst
   168   ord_eq_less_subst
       
   169   forw_subst
   170   back_subst
   170   back_subst
   171   dvd_trans
   171   dvd_trans
   172   rev_mp
   172   rev_mp
   173   mp
   173   mp
   174   set_rev_mp
   174   set_rev_mp
   183   order_antisym
   183   order_antisym
   184   ord_le_eq_trans
   184   ord_le_eq_trans
   185   ord_eq_le_trans
   185   ord_eq_le_trans
   186   ord_less_eq_trans
   186   ord_less_eq_trans
   187   ord_eq_less_trans
   187   ord_eq_less_trans
       
   188   transitive
   188   trans
   189   trans
   189   transitive
       
   190 
   190 
   191 end
   191 end