2008-07-21 chaieb 2008-07-21 Relevant rules added to algebra's context
2008-03-28 wenzelm 2008-03-28 avoid rebinding of existing facts;
2008-03-18 wenzelm 2008-03-18 avoid rebinding of existing facts;
2008-03-05 wenzelm 2008-03-05 explicit referencing of background facts;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2007-10-31 chaieb 2007-10-31 (1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)
2007-07-05 wenzelm 2007-07-05 common normalizer_funs, avoid cterm_of;
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-21 wenzelm 2007-06-21 tuned comments;
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-12 chaieb 2007-06-12 algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
2007-06-11 chaieb 2007-06-11 Conversion for computation on constants now depends on the context
2007-06-11 chaieb 2007-06-11 Added instantiation of algebra method to fields
2007-06-11 chaieb 2007-06-11 explicitely depends on file groebner.ML
2007-06-05 wenzelm 2007-06-05 tuned document;
2007-06-05 wenzelm 2007-06-05 renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
2007-06-05 wenzelm 2007-06-05 Semiring normalization and Groebner Bases.