src/HOL/Groebner_Basis.thy
16 months ago wenzelm 2017-11-26 more symbols;
2016-12-17 haftmann 2016-12-17 reoriented congruence rules in non-explosive direction
2016-10-16 haftmann 2016-10-16 dropped potentially explosive rule for groebner simpset, with no observable effect on examples
2016-10-16 haftmann 2016-10-16 simplified fact references
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-07 wenzelm 2014-11-07 more accurate keywords;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-23 haftmann 2014-10-23 further downshift of theory Parity in the hierarchy
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-05-04 blanchet 2014-05-04 added 'satx' proof method to Try0
2014-02-16 haftmann 2014-02-16 eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
2014-01-30 blanchet 2014-01-30 added 'algebra' and 'meson' to 'try0'
2013-11-04 haftmann 2013-11-04 dropped dead code
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 remove duplicate [algebra] declarations
2012-03-27 huffman 2012-03-27 generalize more div/mod lemmas
2012-03-27 huffman 2012-03-27 generalize some theorems about div/mod
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2010-05-07 haftmann 2010-05-07 delete Groebner_Basis directory -- only one file left
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-06 haftmann 2010-05-06 proper sublocales; no free-floating ML sections
2010-05-06 haftmann 2010-05-06 moved generic lemmas to appropriate places
2010-05-06 haftmann 2010-05-06 dropped duplicate comp_arith
2010-05-06 haftmann 2010-05-06 avoid references to groebner bases in names which have no references to groebner bases
2010-05-06 haftmann 2010-05-06 moved presimplification rules for algebraic methods into named thms functor
2010-05-06 haftmann 2010-05-06 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-05-05 haftmann 2010-05-05 moved nat_arith ot Nat_Numeral: clarified normalizer setup
2010-05-05 haftmann 2010-05-05 dropped unused file
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-04-23 haftmann 2010-04-23 dequalified fact name
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.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