Isabelle Light and Boyer_Moore updates

[PetrosPapapa]

There have been a lot of bug fixes, improvements, and additions in both the Isabelle Light and Boyer_Moore libraries.

Isabelle Light:

• Various bug fixes.
• Some of the less useful tactics have been removed.
• New tactics: X_MATCH_GEN_TAC MATCH_EXISTS_TAC induct_tac GEN_ALL_TAC
• Improved tactics: GENERAL_ASM_TAC (and all assumption rewriting tactics) no longer uses filter (= term comparison) which made it very slow. X_MATCH_CHOOSE_TAC has better error reporting. case_tac has improved type matching.

Boyer_Moore:

• Various bug fixes, particularly with generalization.
• Fixed integration with HOL Light tactic system.
• Improved error reporting for justification errors.
• Improved default settings.
• Rewrite heuristics (and tactics that use them) now accept a list of rewrite lemmas from the command line, in the spirit of HOL Light's REWRITE_TAC.
• Added tactics: BOYER_MOORE_FINAL : Potentially the best combination of heuristics. BM_SAFE_TAC : Only applies the safe heuristics. BMF_TAC : BOYER_MOORE_FINAL as a tactic. BMF_NOEQ_TAC : BMF_TAC without the use_equality_heuristic which is sometimes ineffective.

[jrh13]

Thanks a lot for all the improvements Petros -- I was not paying attention to merge pull requests but finally dealt with them.