Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
Sun, 05 Apr 2009 05:07:10 +0100 |
chaieb |
now deals with devision in fields
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
Mon, 16 Jun 2008 11:47:46 +0200 |
chaieb |
Export a wrapper for all semiring_normalizers
|
file |
diff |
annotate
|
Wed, 28 Nov 2007 09:01:34 +0100 |
haftmann |
dropped legacy ml bindings
|
file |
diff |
annotate
|
Wed, 31 Oct 2007 12:19:43 +0100 |
chaieb |
changed signature according to normalizer_data.ML
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:28:05 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
file |
diff |
annotate
|
Thu, 05 Jul 2007 00:06:18 +0200 |
wenzelm |
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
|
file |
diff |
annotate
|
Tue, 03 Jul 2007 22:27:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 25 Jun 2007 00:36:34 +0200 |
wenzelm |
made type conv pervasive;
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 18:28:16 +0200 |
chaieb |
Conversion for computation on constants now depends on the context
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 18:36:09 +0200 |
wenzelm |
fixed type int vs. integer;
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 16:26:04 +0200 |
wenzelm |
Semiring normalization and Groebner Bases.
|
file |
diff |
annotate
|