| Tue, 03 Nov 2009 16:51:33 +0100 | Christian Urban | simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated | file | diff | annotate |
| Tue, 03 Nov 2009 16:17:19 +0100 | Cezary Kaliszyk | Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP | file | diff | annotate |
| Mon, 02 Nov 2009 18:26:55 +0100 | Christian Urban | split quotient.ML into two files | file | diff | annotate |
| Mon, 02 Nov 2009 18:16:19 +0100 | Christian Urban | slightly saner way of parsing the quotient_def | file | diff | annotate |
| Mon, 02 Nov 2009 15:38:49 +0100 | Christian Urban | changed Type.typ_match to Sign.typ_match | file | diff | annotate |
| Mon, 02 Nov 2009 14:57:56 +0100 | Cezary Kaliszyk | Optimization | file | diff | annotate |
| Mon, 02 Nov 2009 11:15:26 +0100 | Cezary Kaliszyk | Fixed quotdata_lookup. | file | diff | annotate |