NO_THEN : thm_tactical

- STRUCTURE
- SYNOPSIS
- Theorem-tactical which always fails.
- DESCRIPTION
- When applied to a theorem-tactic and a theorem, the theorem-tactical NO_THEN always fails with string `NO_THEN`.
- FAILURE
- Always fails when applied to a theorem-tactic and a theorem (note that it never gets as far as being applied to a goal!)
- USES
- Writing compound tactics or tacticals.
- SEEALSO

HOL Kananaskis-13