# HG changeset patch
# User huffman
# Date 1228435545 28800
# Node ID dc0ab579a5ca5c52a033327a5c8458cf13006000
# Parent  1ff53ff7041dc4eef7bb26dd87afc830c0506e84
remove duplicated lemmas

diff -r 1ff53ff7041d -r dc0ab579a5ca src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Dec 04 13:30:09 2008 -0800
+++ b/src/HOL/Groebner_Basis.thy	Thu Dec 04 16:05:45 2008 -0800
@@ -169,7 +169,11 @@
   proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
-  add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
+  add_nat_number_of
+  diff_nat_number_of
+  mult_nat_number_of
+  eq_nat_number_of
+  less_nat_number_of
 
 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
   by (simp add: numeral_1_eq_1)
@@ -458,7 +462,6 @@
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
-
 subsection{* Groebner Bases for fields *}
 
 interpretation class_fieldgb:
@@ -607,14 +610,6 @@
              @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
              name = "ord_frac_simproc", proc = proc3, identifier = []}
 
-val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
-               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
-
-val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
-                 "add_Suc", "add_number_of_left", "mult_number_of_left",
-                 "Suc_eq_add_numeral_1"])@
-                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
-                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
            @{thm "divide_Numeral1"},
            @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
@@ -630,7 +625,7 @@
 in
 val comp_conv = (Simplifier.rewrite
 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
-              addsimps ths addsimps comp_arith addsimps simp_thms
+              addsimps ths addsimps simp_thms
               addsimprocs field_cancel_numeral_factors
                addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
                             ord_frac_simproc]