src/HOL/Groebner_Basis.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-10-30 haftmann 2009-10-30 combined former theories Divides and IntDiv to one theory Divides
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-04-15 haftmann 2009-04-15 theory NatBin now named Nat_Numeral
2009-04-05 chaieb 2009-04-05 More precise treatement of rational constants by the normalizer for fields
2009-04-05 chaieb 2009-04-05 now deals with devision in fields
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-22 haftmann 2009-03-22 dropped theory Arith_Tools
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-20 nipkow 2009-02-20 removed subsumed lemmas
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-14 ballarin 2008-12-14 Ported HOL and HOL-Library to new locales.
2008-12-12 ballarin 2008-12-12 Merged.
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-09 huffman 2008-12-09 separate neg_simps from rel_simps
2008-12-04 huffman 2008-12-04 remove duplicated lemmas
2008-12-04 huffman 2008-12-04 include iszero_simps in lemmas comp_arith
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-28 ballarin 2008-10-28 Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-09-29 haftmann 2008-09-29 clarified dependencies between arith tools
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.