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