lcp [Thu, 04 May 1995 02:01:49 +0200] rev 1108
case is defined using pattern-matching
lcp [Thu, 04 May 1995 02:01:24 +0200] rev 1107
Modified proofs for new form of 'split'.
lcp [Thu, 04 May 1995 02:00:38 +0200] rev 1106
Added pattern-matching code from CHOL/Prod.thy. Changed
definitions so that split is now defined in terms of fst, snd. Now split is
polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT
identical though, as fsplit(P,z) implied that z was a pair, while split(P,z)
means only P(fst(z),snd(z)).