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  Trindemossen-1