Modified proofs for (q)split, fst, snd for new
definitions. The rule f(q)splitE is now called (q)splitE and is weaker than
before. The rule '(q)split' is now a meta-equality; this required modifying
all proofs involving e.g. split RS trans.
FOLP = IFOLP +
consts
cla :: "[p=>p]=>p"
rules
classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P"
end