| 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 |