More removal of old-style case expression syntax.

Inspired by an e-mail from Hasan, I do "reflection" and derive a
tautology checker (strictly a "unsat-prover") for normal boolean
formulas in HOL. It's hideously slow, but then, we are running the
algorithm in HOL completely unnecessarily.

A quick and hackish mechanisation of DPLL with unit propagation. The
termination argument is probably the nicest thing about it. (Actually, no;
the nicest thing is that we can run DPLL with EVAL for free.)