src/HOL/Groebner_Basis.thy
changeset 36716 b09f3ad3208f
parent 36714 ae84ddf03c58
child 36720 41da7025e59c
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 17:59:20 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 18:16:07 2010 +0200
     1.3 @@ -162,16 +162,6 @@
     1.4  proof
     1.5  qed (simp_all add: algebra_simps)
     1.6  
     1.7 -lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
     1.8 -  by simp
     1.9 -
    1.10 -lemmas semiring_norm =
    1.11 -  Let_def arith_simps nat_arith rel_simps neg_simps if_False
    1.12 -  if_True add_0 add_Suc add_number_of_left mult_number_of_left
    1.13 -  numeral_1_eq_1[symmetric] Suc_eq_plus1
    1.14 -  numeral_0_eq_0[symmetric] numerals[symmetric]
    1.15 -  iszero_simps not_iszero_Numeral1
    1.16 -
    1.17  ML {*
    1.18  local
    1.19  
    1.20 @@ -589,6 +579,8 @@
    1.21  end
    1.22  *}
    1.23  
    1.24 +lemmas comp_arith = semiring_norm (*FIXME*)
    1.25 +
    1.26  
    1.27  subsection {* Groebner Bases *}
    1.28