| Fri, 25 Nov 1994 11:02:39 +0100 | lcp | moved Cantors theorem here from ZF/ex/misc | changeset | files |
| Fri, 25 Nov 1994 10:43:50 +0100 | lcp | deepen_tac: modified due to outcome of experiments. Its | changeset | files |
| Fri, 25 Nov 1994 09:13:49 +0100 | clasohm | added qed_goal[w] | changeset | files |
| Fri, 25 Nov 1994 00:02:37 +0100 | lcp | added blank line | changeset | files |
| Fri, 25 Nov 1994 00:01:04 +0100 | lcp | tidied proofs, using fast_tac etc. as much as possible | changeset | files |
| Fri, 25 Nov 1994 00:00:35 +0100 | lcp | prove_fun: new; no longer depends upon the version in simpdata.ML | changeset | files |
| Thu, 24 Nov 1994 10:57:24 +0100 | lcp | data_domain,Codata_domain: removed replicate; now return one | changeset | files |