src/HOL/Tools/Groebner_Basis/normalizer.ML
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-04-05 chaieb 2009-04-05 now deals with devision in fields
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-06-16 chaieb 2008-06-16 Export a wrapper for all semiring_normalizers
2007-11-28 haftmann 2007-11-28 dropped legacy ml bindings
2007-10-31 chaieb 2007-10-31 changed signature according to normalizer_data.ML
2007-07-20 haftmann 2007-07-20 dropped Nat.ML legacy bindings
2007-07-05 wenzelm 2007-07-05 moved mk_cnumeral/mk_cnumber to Tools/numeral.ML; tuned;
2007-07-03 wenzelm 2007-07-03 tuned;
2007-06-25 wenzelm 2007-06-25 made type conv pervasive;
2007-06-17 chaieb 2007-06-17 normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
2007-06-11 chaieb 2007-06-11 Conversion for computation on constants now depends on the context
2007-06-05 wenzelm 2007-06-05 fixed type int vs. integer;
2007-06-05 wenzelm 2007-06-05 Semiring normalization and Groebner Bases.