src/HOL/Tools/lin_arith.ML
changeset 66610 98b7ba7b1e9a
parent 66035 de6cd60b1226
child 67149 e61557884799
equal deleted inserted replaced
66607:a8edca8c4a68 66610:98b7ba7b1e9a
   973 val setup =
   973 val setup =
   974   init_arith_data
   974   init_arith_data
   975   #> add_discrete_type @{type_name nat}
   975   #> add_discrete_type @{type_name nat}
   976   #> add_lessD @{thm Suc_leI}
   976   #> add_lessD @{thm Suc_leI}
   977   #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
   977   #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
       
   978       @{thm minus_diff_eq},
   978       @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
   979       @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
   979       @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
   980       @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
   980       @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
   981       @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
   981   #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
   982   #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
   982       @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
   983       @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},