[acl2/acl2] 7c4258: Updated hol-in-acl2 library with help from Konrad ...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
https://github.com/acl2/acl2/commit/7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp

Log Message:
-----------
Updated hol-in-acl2 library with help from Konrad Slind. Added eval-events-from-file.

The hol-in-acl2 library is a bit cleaner now, in particular with the
addition of new utility zf::import-theory and files *.defhol generated
(by Konrad) using the hol-to-acl2 translator. Also added a new
utility; see :DOC eval-events-from-file.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing