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 |