Mods to get examples working again.

CASE_TAC no longer worked since I added
non-datatype entries to the TypeBase.
That has been fixed, and better error
messages are now generated from some
of the entrypoints in TypeBase that
expect datatypes.

Also fixed some rotted proofs in
tfl/examples.

Updating some examples, and adding a variation on dfs, where
the graph has a function type but type system nonetheless
ensures that the graph is finite.

Implementation of sha-1. A good exercise for the word libraries, but
it would be difficult to prove correct.

Adding a fast regular expression matcher. Changing old regexp.sml
to live in regexp.naive

Adding a depth-first search algorithm on directed, possibly cyclic,
graphs. Mildly interesting termination argument, due to Scott Owens.