2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-04-05 chaieb 2009-04-05 now deals with devision in fields
2009-02-04 chaieb 2009-02-04 Now catch ERROR exception thrown by find and friends
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-07-21 chaieb 2008-07-21 Tuned and corrected ideal_tac for algebra.
2007-12-05 haftmann 2007-12-05 map_product and fold_product
2007-10-31 chaieb 2007-10-31 (1) signatures updated according to normalizer_data.ML (added field ideal in entry); (2) For a theory the conversions returned are now ring_conv (as before, proves a universal statement), simple_ideal proves ideal membership for one polynomial ; multi_ideal solves the more general ideal membership for several existentially quantifier variables involved in several conjunctions; a simpset containing a simproc to turn x = y into p = 0 where p is the normal form of x - y; (3) Added ideal_tac a tactic to prove general ideal membership (cf. John Harrision CADE 2007) ; (4) Added algebra_tac : first tries ring_tac (old algebra) then ideal_tac
2007-10-08 chaieb 2007-10-08 fixed bug in grobner_ideal
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated, integer);
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality; do not export ring_conv (which is not a conversion anyway); renamed algebra_tac to ring_tac; ring_tac: simplified tactic wrapper, no longer handles ERROR;
2007-07-03 wenzelm 2007-07-03 HOLogic.conj_intr/elims; removed obsolete assocd/assoc; removed dead string_of_pol; tuned;
2007-06-28 haftmann 2007-06-28 dropped Library.lcm
2007-06-25 wenzelm 2007-06-25 made type conv pervasive; Thm.add_cterm_frees;
2007-06-12 chaieb 2007-06-12 Added algebra_tac; tuned;
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.