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