TAUT_TAC : tactic

- STRUCTURE
- SYNOPSIS
- Tautology checker. Proves propositional goals (and instances of them).
- LIBRARY
- taut
- DESCRIPTION
- Given a goal that is an instance of a propositional formula, this tactic will prove the goal provided it is valid. A propositional formula is a term containing only Boolean constants, Boolean-valued variables, Boolean equalities, implications, conjunctions, disjunctions, negations and Boolean-valued conditionals. An instance of a formula is the formula with one or more of the variables replaced by terms of the same type. The tactic accepts goals with or without universal quantifiers for the variables.
- FAILURE
- Fails if the conclusion of the goal is not an instance of a propositional formula or if the instance is not a valid formula.
- SEEALSO

HOL Kananaskis-14