dropped duplicate comp_arith
authorhaftmann
Thu May 06 17:59:19 2010 +0200 (2010-05-06)
changeset 36714ae84ddf03c58
parent 36713 4898bf611209
child 36715 5f612b6d64a8
dropped duplicate comp_arith
NEWS
src/HOL/Groebner_Basis.thy
src/HOL/Tools/Qelim/presburger.ML
src/HOL/ex/Groebner_Examples.thy
     1.1 --- a/NEWS	Thu May 06 17:55:12 2010 +0200
     1.2 +++ b/NEWS	Thu May 06 17:59:19 2010 +0200
     1.3 @@ -140,6 +140,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dropped theorem duplicate comp_arith; use semiring_norm instead.  INCOMPATIBILITY.
     1.8 +
     1.9  * Theory 'Finite_Set': various folding_* locales facilitate the application
    1.10  of the various fold combinators on finite sets.
    1.11  
     2.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 17:55:12 2010 +0200
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 17:59:19 2010 +0200
     2.3 @@ -589,8 +589,6 @@
     2.4  end
     2.5  *}
     2.6  
     2.7 -lemmas comp_arith = semiring_norm (*FIXME*)
     2.8 -
     2.9  
    2.10  subsection {* Groebner Bases *}
    2.11  
     3.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 17:55:12 2010 +0200
     3.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 17:59:19 2010 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  struct
     3.5  
     3.6  open Conv;
     3.7 -val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
     3.8 +val comp_ss = HOL_ss addsimps @{thms semiring_norm};
     3.9  
    3.10  fun strip_objimp ct =
    3.11    (case Thm.term_of ct of
     4.1 --- a/src/HOL/ex/Groebner_Examples.thy	Thu May 06 17:55:12 2010 +0200
     4.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Thu May 06 17:59:19 2010 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4  
     4.5  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
     4.6    apply (simp only: power_Suc power_0)
     4.7 -  apply (simp only: comp_arith)
     4.8 +  apply (simp only: semiring_norm)
     4.9    oops
    4.10  
    4.11  lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"