Mon, 13 Dec 1993 18:48:47 +0100 | lcp | added mention of simplifier, splitter, hypsubst | changeset | files |
Mon, 13 Dec 1993 18:18:34 +0100 | lcp | new year | changeset | files |
Fri, 10 Dec 1993 13:46:38 +0100 | nipkow | updated instantiate to deal with type clashes | changeset | files |
Fri, 10 Dec 1993 10:39:12 +0100 | lcp | ZF/equalities/SUM_eq_UN: new | changeset | files |
Fri, 10 Dec 1993 10:36:39 +0100 | lcp | Pure/tactic/compose_inst_tac: when catching exception THM, prints the | changeset | files |
Thu, 09 Dec 1993 11:39:33 +0100 | nipkow | deleted harmful basify, which pulled rewrite rules down to base type. | changeset | files |