DISJ_CANON_CONV : term -> thm
Puts an iterated disjunction in canonical form.
When applied to a term, DISJ_CANON_CONV splits it into the set of disjuncts
and produces a theorem asserting the equivalence of the term and the new term
with the disjuncts right-associated without repetitions and in a canonical
- FAILURE CONDITIONS
Fails if applied to a non-Boolean term. If applied to a term that is not a
disjunction, it will trivially work in the sense of regarding it as a single
disjunct and returning a reflexive theorem.
# DISJ_CANON_CONV `(c \/ a \/ b) \/ (b \/ a \/ d)`;;
val it : thm = |- (c \/ a \/ b) \/ b \/ a \/ d <=> a \/ b \/ c \/ d
- SEE ALSO
AC, CONJ_CANON_CONV, DISJ_ACI_CONV.