Add (un)set_then_multiple_subgoals to control the behavior of THEN

[aqjune-aws]

This patch adds unset_then_multiple_subgoals and set_then_multiple_subgoals that controls the behavior of THEN with respect to the number of subgoals that its first tactic generated.

This is useful when one wants to check whether a proof written using THEN can be syntactically converted to the e-g form.
If this flag is set to true, t1 THEN t2 THEN .. can be converted to e(t1);; e(t2);; ... (modulo the validity check). To roll back the behavior of THEN to the default version, use set_then_multiple_subgoals.

  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THEN ARITH_TAC);;
  val it : thm = |- x + 1 = 1 + x /\ x + 2 = 2 + x

  # unset_then_multiple_subgoals;;
  val it : bool = false
  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THEN ARITH_TAC);;
  Exception: Failure "seqapply: Length mismatch".
  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THENL [ARITH_TAC; ARITH_TAC]);;
  val it : thm = |- x + 1 = 1 + x /\ x + 2 = 2 + x
  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THENL (replicate ARITH_TAC 2));;
  val it : thm = |- x + 1 = 1 + x /\ x + 2 = 2 + x

Also, this patch adds a Help document for unset_jrh_lexer which was missing (but not set_jrh_lexer for brevity; the command is simply mentioned in unset_jrh_lexer).

[aqjune-aws]

As a sanity check I turned this flag on and ran BIGNUM_COPY_CORRECT and it worked well. :)

[jrh13]

Indeed, this might be quite helpful for those finding the THEN structure with multiple subgoals confusing. And thanks for catching the missing Help file for unset_jrh_lexer!
These are rather special cases where the preprocessor is doing something magical, so maybe it is worth emphasizing that they are not exactly Boolean variables in the usual sense but also not functions, perhaps more like Boolean constants. The latter means that saying "is called" may be a bit confusing without further explanation, even though the example shows it quite explicitly. On the other hand, I am not sure myself how to best clarify it.

[aqjune-aws]

This is my trial to change their types from bool to (preprocessor keyword). :) I omitted their actual OCaml type which is bool because it seemed less important. Also slightly edited the sentences from called to read by a preprocessor.

--

Slightly updated the sentences further to remove usage of 'flag'.

[jrh13]

Thank you, this all looks good now!