| Tue, 12 Sep 2006 16:44:04 +0200 |
huffman |
remove extra dependency
|
changeset |
files
|
| Tue, 12 Sep 2006 14:50:11 +0200 |
wenzelm |
more on terms;
|
changeset |
files
|
| Tue, 12 Sep 2006 12:16:17 +0200 |
wenzelm |
Efficient term substitution -- avoids copying.
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:57 +0200 |
wenzelm |
ctyp: maintain maxidx;
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:55 +0200 |
wenzelm |
removed obsolete aconvs (use eq_list aconv);
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:53 +0200 |
wenzelm |
tuned eq_list;
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:46 +0200 |
wenzelm |
moved term subst functions to TermSubst;
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:39 +0200 |
wenzelm |
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:33 +0200 |
wenzelm |
added Pure/term_subst.ML;
|
changeset |
files
|
| Tue, 12 Sep 2006 12:12:25 +0200 |
wenzelm |
added Gentzen:1935;
|
changeset |
files
|
| Tue, 12 Sep 2006 07:49:07 +0200 |
huffman |
import RealVector
|
changeset |
files
|
| Tue, 12 Sep 2006 06:44:45 +0200 |
huffman |
formalization of vector spaces and algebras over the real numbers
|
changeset |
files
|