[acl2/acl2] 156724: Extend svtv-run theorems to other keyword args

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 1567241348f3688fd49c9737f9481fef19467293
https://github.com/acl2/acl2/commit/1567241348f3688fd49c9737f9481fef19467293
Author: Keshav Kini <kesha...@oracle.com>
Date: 2017-01-15 (Sun, 15 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Extend svtv-run theorems to other keyword args

At some point, more keyword arguments were added to `svtv-run`, but
the theorems associated with `svtv-run` don't account for these
arguments. This commit attempts to fix that situation by generalizing
the `svtv-run` theorems to account for cases where the user used
`:include`, `:simplify`, and `:readable`.


Commit: c3192825eac9b5964d6081e8e6de5ed804777544
https://github.com/acl2/acl2/commit/c3192825eac9b5964d6081e8e6de5ed804777544
Author: Keshav Kini <kesha...@oracle.com>
Date: 2017-01-16 (Mon, 16 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Use `iff` context to avoid `(and ... t)`

Per @solswords's suggestion.


Commit: cc0620681ec2b28549d58972e802a9bfb48f7001
https://github.com/acl2/acl2/commit/cc0620681ec2b28549d58972e802a9bfb48f7001
Author: solswords <ssw...@gmail.com>
Date: 2017-01-17 (Tue, 17 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Merge pull request #683 from kini/svtv-run-kwargs

Extend svtv-run theorems to other keyword args


Compare: https://github.com/acl2/acl2/compare/f53676c87ab6...cc0620681ec2

[GitHub]

Branch: refs/heads/master