1.1 --- a/NEWS	Wed Apr 18 23:57:44 2012 +0200
     1.2 +++ b/NEWS	Tue Apr 17 16:21:47 2012 +1000
     1.3 @@ -521,6 +521,14 @@
     1.4    word_of_int_0_hom ~> word_0_wi
     1.5    word_of_int_1_hom ~> word_1_wi
     1.6  
     1.7 +* New tactic "word_bitwise" for splitting machine word equalities and
     1.8 +inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word
     1.9 +session. Supports addition, subtraction, multiplication, shifting by
    1.10 +constants, bitwise operators and numeric constants. Requires fixed-length word
    1.11 +types, cannot operate on 'a word. Solves many standard word identies outright
    1.12 +and converts more into first order problems amenable to blast or similar. See
    1.13 +HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy.
    1.14 +
    1.15  * Clarified attribute "mono_set": pure declaration without modifying
    1.16  the result of the fact expression.
    1.17