| Thu, 06 May 2010 23:11:57 +0200 |
haftmann |
proper sublocales; no free-floating ML sections
|
file |
diff |
annotate
|
| Thu, 06 May 2010 19:35:43 +0200 |
haftmann |
revert to loose merge semantics
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:09:18 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:06:47 +0200 |
haftmann |
tuned headings
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:02:34 +0200 |
haftmann |
avoid open
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:00:46 +0200 |
haftmann |
tuned internal structure
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:57:59 +0200 |
haftmann |
fail on merge of conflicting normalization entries: functions are not mergable
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:57:28 +0200 |
haftmann |
more canonical data administration
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:53:35 +0200 |
haftmann |
removed former algebra presimpset entirely
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:50:26 +0200 |
haftmann |
removed former algebra presimpset from accessor
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:41:14 +0200 |
haftmann |
removed former algebra presimpset from signature
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:40:02 +0200 |
haftmann |
moved presimplification rules for algebraic methods into named thms functor
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:32:20 +0200 |
haftmann |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 11:47:47 +0100 |
haftmann |
hide fact names clashing with fact names from Group.thy
|
file |
diff |
annotate
|
| 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
|