| Tue, 16 May 2006 18:31:46 +0200 |
wenzelm |
* Pure/library: divide_and_conquer;
|
changeset |
files
|
| Tue, 16 May 2006 18:20:26 +0200 |
paulson |
replaced references to the robot by the mailing list page
|
changeset |
files
|
| Tue, 16 May 2006 14:11:39 +0200 |
urbanc |
added a much simpler proof for the iteration and
|
changeset |
files
|
| Tue, 16 May 2006 13:05:37 +0200 |
wenzelm |
Amine Chaieb: Ferrante and Rackoff Algorithm;
|
changeset |
files
|
| Tue, 16 May 2006 13:05:14 +0200 |
wenzelm |
Sign.certify_sort;
|
changeset |
files
|
| Tue, 16 May 2006 13:01:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 May 2006 13:01:30 +0200 |
wenzelm |
removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);
|
changeset |
files
|
| Tue, 16 May 2006 13:01:29 +0200 |
wenzelm |
avoid low-level Term.str_of_term;
|
changeset |
files
|
| Tue, 16 May 2006 13:01:28 +0200 |
wenzelm |
abstract interfaces for type algebra;
|
changeset |
files
|
| Tue, 16 May 2006 13:01:27 +0200 |
wenzelm |
added divide_and_conquer combinator (by Amine Chaieb);
|
changeset |
files
|
| Tue, 16 May 2006 13:01:26 +0200 |
wenzelm |
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
|
changeset |
files
|
| Tue, 16 May 2006 13:01:24 +0200 |
wenzelm |
more abstract interface to classes/arities;
|
changeset |
files
|