[acl2/acl2] bdfd55: Adapt DEFUN-SK query utilities to change to DEFUN-...
1 view
Skip to first unread message
GitHub
Jul 30, 2016, 12:02:10 AM7/30/16
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: bdfd5534d4b8bf337f409a2fb8df846060353563
https://github.com/acl2/acl2/commit/bdfd5534d4b8bf337f409a2fb8df846060353563
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2016-07-29 (Fri, 29 Jul 2016)
Changed paths:
M books/kestrel/utilities/defun-sk-queries.lisp
Log Message:
-----------
Adapt DEFUN-SK query utilities to change to DEFUN-SK.
Now that DEFUN-SK uses ADD-SUFFIX instead of PACKN to construct the name of the
strengthening theorem of DEFUN-SK, the code of the DEFUN-SK query utilities has
been changed to do that too.
Home: https://github.com/acl2/acl2
Commit: bdfd5534d4b8bf337f409a2fb8df846060353563
https://github.com/acl2/acl2/commit/bdfd5534d4b8bf337f409a2fb8df846060353563
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2016-07-29 (Fri, 29 Jul 2016)
Changed paths:
M books/kestrel/utilities/defun-sk-queries.lisp
Log Message:
-----------
Adapt DEFUN-SK query utilities to change to DEFUN-SK.
Now that DEFUN-SK uses ADD-SUFFIX instead of PACKN to construct the name of the
strengthening theorem of DEFUN-SK, the code of the DEFUN-SK query utilities has
been changed to do that too.
GitHub
Jul 30, 2016, 12:20:56 AM7/30/16
to acl2-...@googlegroups.com
Branch: refs/heads/master
Reply all
Reply to author
Forward
0 new messages