src/HOL/Tools/Groebner_Basis/normalizer.ML
Thu, 06 May 2010 16:32:20 +0200 haftmann dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
Sun, 28 Feb 2010 23:51:31 +0100 wenzelm more antiquotations;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Tue, 09 Feb 2010 11:47:47 +0100 haftmann hide fact names clashing with fact names from Group.thy
Mon, 19 Oct 2009 21:54:57 +0200 wenzelm uniform use of Integer.add/mult/sum/prod;
Wed, 24 Jun 2009 09:41:14 +0200 nipkow corrected and unified thm names
Sun, 05 Apr 2009 05:07:10 +0100 chaieb now deals with devision in fields
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Mon, 16 Jun 2008 11:47:46 +0200 chaieb Export a wrapper for all semiring_normalizers
Wed, 28 Nov 2007 09:01:34 +0100 haftmann dropped legacy ml bindings
Wed, 31 Oct 2007 12:19:43 +0100 chaieb changed signature according to normalizer_data.ML
Fri, 20 Jul 2007 14:28:05 +0200 haftmann dropped Nat.ML legacy bindings
Thu, 05 Jul 2007 00:06:18 +0200 wenzelm moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
Tue, 03 Jul 2007 22:27:25 +0200 wenzelm tuned;
Mon, 25 Jun 2007 00:36:34 +0200 wenzelm made type conv pervasive;
Sun, 17 Jun 2007 13:39:32 +0200 chaieb normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
Mon, 11 Jun 2007 18:28:16 +0200 chaieb Conversion for computation on constants now depends on the context
Tue, 05 Jun 2007 18:36:09 +0200 wenzelm fixed type int vs. integer;
Tue, 05 Jun 2007 16:26:04 +0200 wenzelm Semiring normalization and Groebner Bases.
less more (0) tip