equal
deleted
inserted
replaced
519 word_of_int_succ_hom ~> wi_hom_succ |
519 word_of_int_succ_hom ~> wi_hom_succ |
520 word_of_int_pred_hom ~> wi_hom_pred |
520 word_of_int_pred_hom ~> wi_hom_pred |
521 word_of_int_0_hom ~> word_0_wi |
521 word_of_int_0_hom ~> word_0_wi |
522 word_of_int_1_hom ~> word_1_wi |
522 word_of_int_1_hom ~> word_1_wi |
523 |
523 |
|
524 * New tactic "word_bitwise" for splitting machine word equalities and |
|
525 inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word |
|
526 session. Supports addition, subtraction, multiplication, shifting by |
|
527 constants, bitwise operators and numeric constants. Requires fixed-length word |
|
528 types, cannot operate on 'a word. Solves many standard word identies outright |
|
529 and converts more into first order problems amenable to blast or similar. See |
|
530 HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy. |
|
531 |
524 * Clarified attribute "mono_set": pure declaration without modifying |
532 * Clarified attribute "mono_set": pure declaration without modifying |
525 the result of the fact expression. |
533 the result of the fact expression. |
526 |
534 |
527 * "Transitive_Closure.ntrancl": bounded transitive closure on |
535 * "Transitive_Closure.ntrancl": bounded transitive closure on |
528 relations. |
536 relations. |