[acl2/acl2] f74a46: bitops/merge: add theorems showing specific merges...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: f74a46bd605b15f8c3e250151dfe33c9a7634642
https://github.com/acl2/acl2/commit/f74a46bd605b15f8c3e250151dfe33c9a7634642
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-08-15 (Mon, 15 Aug 2016)

Changed paths:
M books/centaur/bitops/merge.lisp

Log Message:
-----------
bitops/merge: add theorems showing specific merges (e.g. merge-4-bytes) equal to calls of merge-unsigned


Commit: 94ec85faede01d2d17ca613e10f072bba6d182d5
https://github.com/acl2/acl2/commit/94ec85faede01d2d17ca613e10f072bba6d182d5
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-08-15 (Mon, 15 Aug 2016)

Changed paths:
M books/projects/x86isa/machine/guard-helpers.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-arithmetic-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-bitscan-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-convert-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-logical-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mov-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mxcsr-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-shuffle-and-unpack-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-simd-integer-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-arith-and-logic-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-bit-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-conditional-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-divide-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-exchange-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-jump-and-loop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-move-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-multiply-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-push-and-pop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-rotate-and-shift-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-segmentation-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-subroutine-instructions.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-programmer-level-memory.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/testing'


Compare: https://github.com/acl2/acl2/compare/e7f7e45fa583...94ec85faede0

[GitHub]

Branch: refs/heads/master