| Sat, 01 Nov 1997 13:02:19 +0100 |
paulson |
New syntax function for types
|
file |
diff |
annotate
|
| Tue, 28 Oct 1997 17:29:48 +0100 |
wenzelm |
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
|
file |
diff |
annotate
|
| Tue, 21 Oct 1997 17:47:50 +0200 |
wenzelm |
made Poly/ML happy, but SML/NJ unhappy;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 17:08:18 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 18:29:43 +0200 |
wenzelm |
eliminated raise_term;
|
file |
diff |
annotate
|
| Wed, 16 Apr 1997 18:16:45 +0200 |
wenzelm |
tuned type of eq_ix, mem_ix;
|
file |
diff |
annotate
|
| Fri, 14 Mar 1997 10:35:30 +0100 |
nipkow |
Avoid eta-contraction in the simplifier.
|
file |
diff |
annotate
|
| Fri, 07 Mar 1997 10:24:26 +0100 |
paulson |
Improved indentation of aconv
|
file |
diff |
annotate
|
| Tue, 04 Feb 1997 10:33:58 +0100 |
paulson |
Gradual switching to Basis Library functions nth, drop, etc.
|
file |
diff |
annotate
|
| Mon, 18 Nov 1996 16:28:40 +0100 |
paulson |
Optimizations: removal of polymorphic equality; one-argument case
|
file |
diff |
annotate
|
| Wed, 13 Nov 1996 10:42:50 +0100 |
paulson |
Removal of polymorphic equality via mem, subset, eq_set, etc
|
file |
diff |
annotate
|
| Tue, 12 Nov 1996 11:40:41 +0100 |
paulson |
Changed some mem and ins calls to be monomorphic
|
file |
diff |
annotate
|
| Fri, 01 Nov 1996 15:32:03 +0100 |
paulson |
maxidx_of_typs replaces max o map maxidx_of_typ
|
file |
diff |
annotate
|
| Wed, 30 Oct 1996 11:19:09 +0100 |
paulson |
Changed some mem calls to mem_string for greater efficiency (not that it could matter)
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Thu, 28 Dec 1995 12:36:05 +0100 |
paulson |
Updated comments for compression functions
|
file |
diff |
annotate
|
| Fri, 22 Dec 1995 10:48:59 +0100 |
paulson |
Addition of compression, that is, sharing.
|
file |
diff |
annotate
|
| Fri, 08 Dec 1995 10:25:26 +0100 |
paulson |
type_of1: improved error messages
|
file |
diff |
annotate
|
| Thu, 23 Nov 1995 12:18:16 +0100 |
clasohm |
files now define a structure to allow SML/NJ to optimize the code
|
file |
diff |
annotate
|
| Wed, 12 Apr 1995 13:53:34 +0200 |
nipkow |
term.ML: add_loose_bnos now returns a list w/o duplicates.
|
file |
diff |
annotate
|
| Mon, 13 Mar 1995 09:38:10 +0100 |
nipkow |
Changed treatment of during type inference internally generated type
|
file |
diff |
annotate
|
| Tue, 22 Nov 1994 23:30:49 +0100 |
lcp |
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
|
file |
diff |
annotate
|
| Wed, 18 May 1994 15:20:54 +0200 |
wenzelm |
added logicC: class, logicS: sort;
|
file |
diff |
annotate
|
| Thu, 21 Oct 1993 14:38:06 +0100 |
lcp |
Pure/term/fastype_of1: renamed from fastype_of
|
file |
diff |
annotate
|
| Fri, 08 Oct 1993 12:33:17 +0100 |
wenzelm |
added raise_type: string -> typ list -> term list -> 'a;
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|