[Hol-checkins] CVS: hol98/src/n_bit/help/entries wordnLib.WORD_EQ_TAC.doc,NONE,1.1

[Konrad S. <sl...@us...>]

Update of /cvsroot/hol/hol98/src/n_bit/help/entries
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv379/help/entries

Added Files:
	wordnLib.WORD_EQ_TAC.doc 
Log Message:
Documentation for WORD_EQ_TAC.



--- NEW FILE: wordnLib.WORD_EQ_TAC.doc ---
\DOC WORD_EQ_TAC

\TYPE {WORD_EQ_TAC : tactic}

\SYNOPSIS
Proves equality of boolean word expressions.

\DESCRIBE
When {WORD_EQ_TAC} is applied to a goal of the form
{
   !w1 ... xn. M = N
}
where {M} and {N} are built from the word operations
{AND}, {OR}, {EOR}, and {NOT}, it attempts to decide the
equality, failing if {M} and {N} are not able to be proven
equal by using simple algebra.

\EXAMPLE
An application of {WORD_EQ_TAC} solves the goal
{
?- !w1 w2. NOT(w1 & w2) = NOT(w1) | NOT(w2)
}
quickly:
{
- e WORD_EQ_TAC;
OK..
> val it =
    Initial goal proved.
    |- !w1 w2. NOT (w1 & w2) = NOT w1 | NOT w2 : goalstack
}

\COMMENTS
Only available after running {mkword.exe}.

\SEEALSO
wordnLib.WORD_CONV

\ENDDOC