Fri, 13 Jan 1995 02:00:43 +0100 | lcp | Corrected indexing of *datatype | changeset | files |
Thu, 12 Jan 1995 10:53:42 +0100 | lcp | prove_fun now includes equalityI. Added the rewrite rules | changeset | files |
Thu, 12 Jan 1995 10:39:47 +0100 | lcp | Proved sum_bij, sum_ord_iso_cong, prod_bij, | changeset | files |