| Thu, 04 May 1995 02:01:49 +0200 | lcp | case is defined using pattern-matching | changeset | files |
| Thu, 04 May 1995 02:01:24 +0200 | lcp | Modified proofs for new form of 'split'. | changeset | files |
| Thu, 04 May 1995 02:00:38 +0200 | lcp | Added pattern-matching code from CHOL/Prod.thy. Changed | changeset | files |
| Wed, 03 May 1995 17:38:27 +0200 | lcp | Modified proofs for (q)split, fst, snd for new | changeset | files |