| Tue, 30 Apr 1996 12:03:01 +0200 |
clasohm |
moved dest_cimplies to drule.ML; added adjust_maxidx
|
file |
diff |
annotate
|
| Thu, 21 Mar 1996 11:05:34 +0100 |
paulson |
Printing & string functions moved to display.ML
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:08:49 +0100 |
paulson |
Elimination of fully-functorial style.
|
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
|
| Mon, 15 Jan 1996 15:47:10 +0100 |
wenzelm |
improved printing of errors in 'defs';
|
file |
diff |
annotate
|
| Thu, 11 Jan 1996 10:29:31 +0100 |
nipkow |
Removed bug in type unification. Negative indexes are not used any longer.
|
file |
diff |
annotate
|
| Fri, 22 Dec 1995 10:19:55 +0100 |
paulson |
Now "standard" compresses theorems (for sharing).
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:27:48 +0200 |
clasohm |
added same_sg and same_thm
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:08:55 +0200 |
wenzelm |
adapted to new version of shyps-stuff;
|
file |
diff |
annotate
|
| Tue, 01 Aug 1995 17:20:42 +0200 |
wenzelm |
modified pretty_thm, standard, eq_thm to handle shyps;
|
file |
diff |
annotate
|
| Tue, 25 Jul 1995 17:03:16 +0200 |
lcp |
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
|
file |
diff |
annotate
|
| Tue, 14 Mar 1995 10:40:04 +0100 |
nipkow |
Removed an old bug which made some simultaneous instantiations fail if they
|
file |
diff |
annotate
|
| Mon, 13 Mar 1995 09:38:10 +0100 |
nipkow |
Changed treatment of during type inference internally generated type
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|