Theorem-tactical which always fails.
When applied to a theorem-tactic and a theorem, the theorem-tactical
NO_THEN always fails with Failwith "NO_THEN".
- FAILURE CONDITIONS
Always fails when applied to a theorem-tactic and a theorem (note that it
never gets as far as being applied to a goal!)
Writing compound tactics or tacticals.
- SEE ALSO
ALL_TAC, ALL_THEN, FAIL_TAC, NO_TAC.