swapping out "theorem" in favour of "fetch".

Final fixes to separate schematic definitions from ordinary ones.
Also, some of the examples have been polished a bit.

New additions to proplog - CNF plus a few trivial proofs.

nested.scheme gives a solution to a problem posed by Paulson in
his "ML for The Working Programmer Book".