                 => ThmTactic HOLThm cls thry -> thm -> Tactic cls thry
_CONJUNCTS_THEN' ttac cth g =
  do th1 <- ruleCONJUNCT1 cth
     th2 <- ruleCONJUNCT2 cth
     (ttac th1 `_THEN` ttac th2) g

ruleIMPLICATE :: BoolCtxt thry => HOLTerm -> HOL cls thry HOLThm
ruleIMPLICATE (Neg t') = 
    ruleCONV (convRAND convBETA) $ ruleAP_THM defNOT t'
ruleIMPLICATE _ = throwM $! HOLExhaustiveWarning "ruleIMPLICATE"

tacRIGHT_REVERSIBLE :: BoolCtxt thry => Tactic cls thry
tacRIGHT_REVERSIBLE = 
    _FIRST [ tacCONJ