# HG changeset patch # User paulson # Date 1119275662 -7200 # Node ID b24c820a0b85c5c8fb8f5ee488920dd2e9722305 # Parent 40c4653a30d5191075d61f65ec20e8aec282c663 moving some generic inequalities from integer arith to nat arith diff -r 40c4653a30d5 -r b24c820a0b85 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Mon Jun 20 11:45:40 2005 +0200 +++ b/src/HOL/Integ/int_arith1.ML Mon Jun 20 15:54:22 2005 +0200 @@ -504,9 +504,7 @@ minus_mult_left RS sym, minus_mult_right RS sym, minus_add_distrib, minus_minus, mult_assoc, of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult, - of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat, - zero_neq_one, zero_less_one, zero_le_one, - zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; + of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]; val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@ Int_Numeral_Simprocs.cancel_numerals; diff -r 40c4653a30d5 -r b24c820a0b85 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Mon Jun 20 11:45:40 2005 +0200 +++ b/src/HOL/arith_data.ML Mon Jun 20 15:54:22 2005 +0200 @@ -388,7 +388,8 @@ val add_rules = [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, One_nat_def,isolateSuc, - order_less_irrefl]; + order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, + zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1,