Various doc fixes

extra semicolons removed from (some) .sig files

Prim_rec: whitespace cleanup in both .sig and .doc

New prove_case_eq_thm entrypoint for Prim_rec

Implement function to prove a case-constant elimination rewrite

Implement and document a new prove_case_rand_thm function in Prim_rec.

This will be the basis for a general tool that moves case-constants up
within a term and then eliminates them, subsuming, for example, the
functionality in boolSimps.COND_elim_ss, which does this but only for
the boolean case-constant (aka if-then-else).

Clean up code that relies on constant and theorem names for case constants.

Rather than code having to know that the constant is called
“type_CASE” and that its definition is stored in “type_case_def”, use
ML entrypoints in Prim_rec to abstract these details.

This is progress with github issue #97.

Change src/bool to src/1 as a prelude to experimentation!