Document the new sequent proof mode and its operations

[robdockins]

PR #1689 reworked the proof mode in SAW to operate on sequents instead of just propositions, and added a variety of tactics for manipulating them, similar in many ways to the tactics found in an interactive theorem prover. The new proof mode and the operations that manipulate it need to be documented in a more coherent way than just the help text for the individual operations.

For reference a (I think) complete listing of the new sequent-oriented commands is listed here:

• enable_sequent_goals / disable_sequent_goals
• prove_by_bv_induction for induction on bitvector values (not strictly sequent related, but difficult to handle without sequents)
• simplify_local for rewriting by local hypotheses
• unfocus, focus_hyp, focus_concl focus manipulation
• normalize_sequent automatic application of reversible sequent rules
• delete_hyps, retain_hyps, delete_concl, retain_concl weakening rules
• goal_cut sequent cut rule/statement of intermediate lemmas
• goal_intro_hyp, goal_intro_hyps implication introduction
• goal_revert_hyp undoing implication introduction
• goal_split splitting into subgoals along conjunction, disjunction, if/then/else or implication
• goal_apply, goal_apply_hyp applying theorems and hypotheses
• goal_insert, goal_insert_and_specialize introduce theorems as local hypotheses
• goal_specialize_hyp instantiation of universal quantifiers
• goal_intro universal introduction
• print_focus for printing the focused point of a sequent
• addsimp_shallow for "shallow" rewriting
• new term manipulation primitives: generalize_term, implies_term

[robdockins]

Some things that might be nice to add:

• a more gentle tactic than normalize_sequent, or change it's behavior to only normalize in a focus point if focused
• some kind of bracketing tactic similar to Coq's subgoal braces. This would help ensure that tactics intended to handle one subgoal don't "leak" into the proof of others if things change.
• some way to view and rearrange the order in which subgoals are handled.
• better tactics for chains of equational reasoning